[isabelle-dev] construction of the real numbers

[Makarius]

On Mon, 10 May 2010, Brian Huffman wrote:

> 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.

OK, very good.


 	Makarius