[isabelle-dev] construction of the real numbers
makarius at sketis.net
Mon May 10 17:48:10 CEST 2010
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.
More information about the isabelle-dev