src/HOL/ex/Dedekind_Real.thy
2011-01-13 wenzelm 2011-01-13 eliminated global prems; tuned proofs;
2010-11-30 haftmann 2010-11-30 adaptions to changes in Equiv_Relation.thy
2010-10-01 haftmann 2010-10-01 constant `contents` renamed to `the_elem`
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-06-08 haftmann 2010-06-08 tuned quotes, antiquotations and whitespace
2010-05-10 huffman 2010-05-10 add more credits to ex/Dedekind_Real.thy
2010-05-10 huffman 2010-05-10 put construction of reals using Dedekind cuts in HOL/ex