src/HOL/RComplete.thy
Wed, 18 Apr 2012 14:29:19 +0200 hoelzl add lemma to equate floor and div
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Sat, 25 Feb 2012 09:07:41 +0100 bulwahn removing unnecessary assumptions in RComplete;
Sat, 24 Dec 2011 15:53:09 +0100 haftmann tuned proofs
Sun, 04 Sep 2011 06:56:10 -0700 huffman remove unused assumptions from natceiling lemmas
Sun, 04 Sep 2011 06:27:59 -0700 huffman move lemmas nat_le_iff and nat_mono into Int.thy
Sat, 03 Sep 2011 11:10:38 -0700 huffman remove unused assumption from lemma posreal_complete
Sat, 03 Sep 2011 08:01:49 -0700 huffman shorten some proofs
Fri, 02 Sep 2011 20:58:31 -0700 huffman remove redundant simp rules ceiling_floor and floor_ceiling
Fri, 02 Sep 2011 16:48:30 -0700 huffman remove redundant lemma reals_complete2 in favor of complete_real
Fri, 02 Sep 2011 15:19:59 -0700 huffman simplify proof of Rats_dense_in_real;
Fri, 02 Sep 2011 14:27:55 -0700 huffman remove unused, unnecessary lemmas
Fri, 14 Jan 2011 15:44:47 +0100 wenzelm eliminated global prems;
Mon, 19 Jul 2010 16:09:44 +0200 haftmann diff_minus subsumes diff_def
Tue, 18 May 2010 19:00:55 -0700 huffman remove several redundant lemmas about floor and ceiling
Tue, 11 May 2010 09:10:31 -0700 huffman move floor lemmas from RealPow.thy to RComplete.thy
Mon, 10 May 2010 12:12:58 -0700 huffman new construction of real numbers using Cauchy sequences
Thu, 04 Mar 2010 17:28:45 +0100 hoelzl Added natfloor and floor rules for multiplication and power.
Fri, 05 Feb 2010 14:33:50 +0100 haftmann more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Fri, 25 Sep 2009 13:47:28 +0100 paulson New lemmas involving the real numbers, especially limits and series
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Thu, 26 Feb 2009 20:56:59 +0100 wenzelm standard headers;
Thu, 26 Feb 2009 06:21:31 -0800 huffman disable floor_minus and ceiling_minus [simp]
Wed, 25 Feb 2009 11:29:59 -0800 huffman generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
Wed, 28 Jan 2009 16:29:16 +0100 nipkow Replaced group_ and ring_simps by algebra_simps;
Wed, 03 Dec 2008 15:58:44 +0100 haftmann made repository layout more coherent with logical distribution structure; stripped some $Id$s
less more (0) tip