src/HOL/Real/RealDef.thy
Sun, 24 Jun 2007 20:55:41 +0200 nipkow tuned and used field_simps
Sat, 23 Jun 2007 19:33:22 +0200 nipkow tuned and renamed group_eq_simps and ring_eq_simps
Wed, 20 Jun 2007 17:28:55 +0200 huffman remove simp attribute from of_nat_diff, for backward compatibility with zdiff_int
Wed, 20 Jun 2007 05:18:39 +0200 huffman change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
Thu, 07 Jun 2007 04:33:15 +0200 huffman remove redundant lemmas
Thu, 07 Jun 2007 03:45:56 +0200 huffman remove references to preal-specific theorems
Thu, 07 Jun 2007 03:11:31 +0200 huffman define (1::preal); clean up instance declarations
Sat, 19 May 2007 13:41:13 +0200 nipkow added code generation based on Isabelle's rat type.
Mon, 14 May 2007 18:48:24 +0200 huffman move lemmas to RealPow.thy; tuned proofs
Mon, 14 May 2007 09:33:18 +0200 huffman remove redundant lemmas
Mon, 14 May 2007 08:15:13 +0200 huffman cleaned up
Fri, 16 Mar 2007 21:32:12 +0100 haftmann added lattice definitions
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
Sat, 16 Sep 2006 19:12:03 +0200 huffman define new constant of_real for class real_algebra_1;
Wed, 06 Sep 2006 13:48:02 +0200 haftmann got rid of Numeral.bin type
Wed, 26 Jul 2006 19:23:04 +0200 webertj linear arithmetic splits certain operators (e.g. min, max, abs)
Fri, 02 Jun 2006 23:22:29 +0200 wenzelm misc cleanup;
Sun, 12 Feb 2006 12:29:01 +0100 kleing * include generalised MVT in HyperReal (contributed by Benjamin Porter)
Mon, 01 Aug 2005 19:20:26 +0200 wenzelm simprocs: Simplifier.inherit_bounds;
Tue, 19 Jul 2005 17:24:09 +0200 avigad added list of theorem changes to NEWS
Wed, 13 Jul 2005 19:49:07 +0200 avigad Additions to the Real (and Hyperreal) libraries:
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Wed, 04 May 2005 10:42:43 +0200 nipkow fixed lin.arith
Mon, 21 Feb 2005 19:23:46 +0100 nipkow more fine tuniung
Tue, 05 Oct 2004 15:30:50 +0200 paulson new simprules for abs and for things like a/b<1
Wed, 01 Sep 2004 15:04:01 +0200 paulson new "respects" syntax for quotienting
Wed, 18 Aug 2004 11:09:40 +0200 nipkow import -> imports
Mon, 16 Aug 2004 14:22:27 +0200 nipkow New theory header syntax.
Thu, 29 Jul 2004 16:57:41 +0200 paulson removal of more iff-rules from RealDef.thy
Thu, 29 Jul 2004 16:14:42 +0200 paulson removed some [iff] declarations from RealDef.thy, concerning inequalities
less more (0) -50 -30 tip