src/HOL/SupInf.thy
Fri, 02 Mar 2012 09:35:33 +0100 bulwahn removing finiteness goals
Sat, 24 Dec 2011 15:53:09 +0100 haftmann tuned proofs
Fri, 02 Sep 2011 16:57:51 -0700 huffman speed up extremely slow metis proof of Sup_real_iff
Fri, 02 Sep 2011 16:48:30 -0700 huffman remove redundant lemma reals_complete2 in favor of complete_real
Mon, 19 Jul 2010 16:09:44 +0200 haftmann diff_minus subsumes diff_def
Mon, 12 Jul 2010 08:58:13 +0200 haftmann dropped superfluous [code del]s
Sun, 09 May 2010 17:47:43 -0700 huffman avoid using real-specific versions of generic lemmas
Sun, 28 Mar 2010 10:34:02 -0700 huffman cleaned up some proofs
Thu, 18 Mar 2010 13:56:34 +0100 haftmann dropped odd interpretation of comm_monoid_mult into comm_monoid_add
Thu, 04 Mar 2010 19:50:45 +0100 hoelzl Supremum and Infimum on real intervals
Thu, 18 Feb 2010 14:21:44 -0800 huffman get rid of many duplicate simp rule warnings
Mon, 08 Feb 2010 14:06:54 +0100 haftmann moved auxiliary lemmas to more appropriate places
Fri, 05 Feb 2010 14:33:50 +0100 haftmann more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
Fri, 13 Nov 2009 14:14:04 +0100 nipkow renamed lemmas "anti_sym" -> "antisym"
Wed, 11 Nov 2009 14:04:56 +0000 paulson Added two new lemmas
Wed, 28 Oct 2009 11:42:31 +0000 paulson New theory Probability, which contains a development of measure theory
Tue, 27 Oct 2009 12:59:57 +0000 paulson New theory SupInf of the supremum and infimum operators for sets of reals.
less more (0) tip