src/HOL/ex/Dedekind_Real.thy
2012-03-25 ago merged fork with new numeral representation (see NEWS)
2012-03-13 ago prefer abs_def over def_raw;
2011-11-30 ago prefer typedef without extra definition and alternative name;
2011-01-13 ago eliminated global prems;
2010-11-30 ago adaptions to changes in Equiv_Relation.thy
2010-10-01 ago constant `contents` renamed to `the_elem`
2010-07-12 ago dropped superfluous [code del]s
2010-06-08 ago tuned quotes, antiquotations and whitespace
2010-05-10 ago add more credits to ex/Dedekind_Real.thy
2010-05-10 ago put construction of reals using Dedekind cuts in HOL/ex