src/HOL/ex/Dedekind_Real.thy
Fri, 19 Oct 2012 15:12:52 +0200 webertj Renamed {left,right}_distrib to distrib_{right,left}.
Fri, 12 Oct 2012 18:58:20 +0200 wenzelm discontinued obsolete typedef (open) syntax;
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Tue, 13 Mar 2012 16:56:56 +0100 wenzelm prefer abs_def over def_raw;
Wed, 30 Nov 2011 16:27:10 +0100 wenzelm prefer typedef without extra definition and alternative name;
Thu, 13 Jan 2011 23:50:16 +0100 wenzelm eliminated global prems;
Tue, 30 Nov 2010 17:19:11 +0100 haftmann adaptions to changes in Equiv_Relation.thy
Fri, 01 Oct 2010 16:05:25 +0200 haftmann constant `contents` renamed to `the_elem`
Mon, 12 Jul 2010 08:58:13 +0200 haftmann dropped superfluous [code del]s
Tue, 08 Jun 2010 16:37:22 +0200 haftmann tuned quotes, antiquotations and whitespace
Mon, 10 May 2010 11:47:56 -0700 huffman add more credits to ex/Dedekind_Real.thy
Mon, 10 May 2010 11:30:05 -0700 huffman put construction of reals using Dedekind cuts in HOL/ex
less more (0) tip