src/HOL/Library/Extended_Real.thy
Thu, 10 Jan 2013 21:22:11 +0100 noschinl added some ereal_of_enat_* lemmas (from $AFP/thys/Girth_Chromatic)
Fri, 16 Nov 2012 18:45:57 +0100 hoelzl move theorems to be more generally useable
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Thu, 22 Mar 2012 16:44:19 +0100 wenzelm tuned proofs;
Tue, 20 Dec 2011 11:40:56 +0100 noschinl add simp rules for enat and ereal
Mon, 05 Dec 2011 17:33:57 +0100 hoelzl real is better supported than real_of_nat, use it in the nat => ereal coercion
Fri, 21 Oct 2011 14:25:38 +0200 bulwahn replacing metis proofs with facts xt1 by new proof with more readable names
Wed, 21 Sep 2011 08:28:53 -0700 huffman remove redundant instantiation ereal :: power
Wed, 14 Sep 2011 10:08:52 -0400 hoelzl renamed Complete_Lattices lemmas, removed legacy names
Tue, 13 Sep 2011 16:21:48 +0200 noschinl tune simpset for Complete_Lattices
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Fri, 02 Sep 2011 16:48:30 -0700 huffman remove redundant lemma reals_complete2 in favor of complete_real
Thu, 25 Aug 2011 11:56:20 -0700 huffman remove duplicate simp declaration
Fri, 12 Aug 2011 09:17:24 -0700 huffman make Multivariate_Analysis work with separate set type
Wed, 10 Aug 2011 18:02:16 -0700 huffman avoid warnings about duplicate rules
Thu, 21 Jul 2011 22:47:13 +0200 haftmann moved some lemmas
Thu, 21 Jul 2011 18:40:31 +0200 haftmann ereal is a complete_linorder instance
Wed, 20 Jul 2011 15:42:23 +0200 hoelzl add code generator setup and tests for ereal
Tue, 19 Jul 2011 14:38:48 +0200 hoelzl rename Fin to enat
Tue, 19 Jul 2011 14:38:29 +0200 hoelzl add ereal to typeclass infinity
Tue, 19 Jul 2011 14:36:12 +0200 hoelzl Rename extreal => ereal
less more (0) tip