src/HOL/RComplete.thy
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