[isabelle-dev] Evaluation of floor and ceiling

Brian Huffman brianh at cs.pdx.edu
Sat Jul 9 21:00:24 CEST 2011


On Sat, Jul 9, 2011 at 10:51 AM, Lukas Bulwahn <bulwahn at in.tum.de> wrote:
> I think it is reasonable, so I added your changeset and set up the code
> generator and added a simple test case for quickcheck showing that we can
> evaluate floor and ceiling now.
> These preliminary changesets can be inspected under
> http://isabelle.in.tum.de/testboard/Isabelle, and I will push them into the
> mainstream repository, once the tests ran through.
>
> @Brian: Thanks for your effort.
>
> Lukas

Thanks for taking care of this. I also want to point out that since
this is a user-visible change to the libraries (floor and ceiling are
in a different class now) an entry should be added to the NEWS file,
if you haven't created one already.

- Brian



More information about the isabelle-dev mailing list