[isabelle-dev] construction of the real numbers

[Brian Huffman]

On Mon, May 10, 2010 at 3:59 AM, Makarius <makarius at sketis.net> wrote:
> This means there are about 1-2 weeks left for bigger changes.  Do you manage
> to exchange the reals by then?

I can do it today. I have already exchanged the reals and tested
everything in a local clone of the Isabelle repo. I haven't created
Dedekind_Real.thy yet, but that shouldn't take long.

> How is the timing for your theories?  Is there an impact on AFP, for
> example.  The latter can be taken as an indication how it will affect other
> users out there.

The new development no longer includes separate lemmas like
"real_mult_assoc", "real_le_linear", etc -- these are proved directly
within the instance proofs. Having to replace these theorem names with
the generic ones like "mult_assoc" and "linear" is the only effect on
user theories that I've seen. I could add a list of "legacy theorem
names" (like what Int.thy has) for backward compatibility.

There are no theories in the distribution of the AFP that use type
"preal". If there are any end-users that use this type, well, they can
define it themselves in terms of type "real" if they really want to.

- Brian