src/HOL/Library/Extended_Real.thy
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-03-22 wenzelm 2012-03-22 tuned proofs;
2011-12-20 noschinl 2011-12-20 add simp rules for enat and ereal
2011-12-05 hoelzl 2011-12-05 real is better supported than real_of_nat, use it in the nat => ereal coercion
2011-10-21 bulwahn 2011-10-21 replacing metis proofs with facts xt1 by new proof with more readable names
2011-09-21 huffman 2011-09-21 remove redundant instantiation ereal :: power
2011-09-14 hoelzl 2011-09-14 renamed Complete_Lattices lemmas, removed legacy names
2011-09-13 noschinl 2011-09-13 tune simpset for Complete_Lattices
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-09-02 huffman 2011-09-02 remove redundant lemma reals_complete2 in favor of complete_real
2011-08-25 huffman 2011-08-25 remove duplicate simp declaration
2011-08-12 huffman 2011-08-12 make Multivariate_Analysis work with separate set type
2011-08-10 huffman 2011-08-10 avoid warnings about duplicate rules
2011-07-21 haftmann 2011-07-21 moved some lemmas
2011-07-21 haftmann 2011-07-21 ereal is a complete_linorder instance
2011-07-20 hoelzl 2011-07-20 add code generator setup and tests for ereal
2011-07-19 hoelzl 2011-07-19 rename Fin to enat
2011-07-19 hoelzl 2011-07-19 add ereal to typeclass infinity
2011-07-19 hoelzl 2011-07-19 Rename extreal => ereal