On 07/08/2011 03:13 AM, Brian Huffman wrote:
I wrote to Florian about this exact issue back in February 2010.
Florian's recommended solution at the time was to add a new subclass
of archimedean_field that fixes the floor function and assumes a
correctness property about it. This solution is really easy to
implement (see attached diff). If people think this is a reasonable
design, then I'll let someone else go ahead and test and commit the
patch.
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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
