src/HOL/ex/Dedekind_Real.thy
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-11 Thomas Sewell 2014-06-11 Hypsubst preserves equality hypotheses Fixes included for various theories affected by this change.
2014-04-12 nipkow 2014-04-12 made mult_pos_pos a simp rule
2013-12-25 haftmann 2013-12-25 prefer more canonical names for lemmas on min/max
2013-11-05 hoelzl 2013-11-05 move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-09-03 wenzelm 2013-09-03 proper imports; tuned proofs;
2013-08-27 hoelzl 2013-08-27 renamed typeclass dense_linorder to unbounded_dense_linorder
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-03-13 wenzelm 2012-03-13 prefer abs_def over def_raw;
2011-11-30 wenzelm 2011-11-30 prefer typedef without extra definition and alternative name; tuned proofs;
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