src/HOL/Real/real_arith.ML
Sat, 29 Jul 2006 13:15:12 +0200 webertj lin_arith_prover splits certain operators (e.g. min, max, abs)
Thu, 19 Jan 2006 21:22:08 +0100 wenzelm setup: theory -> theory;
Mon, 17 Oct 2005 23:10:13 +0200 wenzelm change_claset/simpset;
Thu, 14 Jul 2005 17:16:52 +0200 wenzelm accomodate change of real_of_XXX;
Wed, 04 May 2005 10:42:43 +0200 nipkow fixed lin.arith
Thu, 07 Apr 2005 09:25:33 +0200 wenzelm reverted renaming of Some/None in comments and strings;
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Tue, 07 Sep 2004 13:41:30 +0200 nipkow fixed discrete field.
Mon, 06 Sep 2004 17:37:35 +0200 nipkow made mult_mono_thms generic.
Thu, 24 Jun 2004 17:52:02 +0200 paulson replaced monomorphic abs definitions by abs_if
Tue, 30 Mar 2004 11:25:14 +0200 paulson tidied
Thu, 25 Mar 2004 10:31:25 +0100 paulson new treatment of equivalence classes
Fri, 19 Mar 2004 10:50:06 +0100 paulson removed redundant thms
Tue, 02 Mar 2004 11:06:37 +0100 paulson fixed bugs in the setup of arithmetic procedures
Tue, 17 Feb 2004 10:41:59 +0100 paulson further tweaks to the numeric theories
Sun, 15 Feb 2004 10:46:37 +0100 paulson Polymorphic treatment of binary arithmetic using axclasses
Wed, 28 Jan 2004 17:01:01 +0100 paulson tidying up arithmetic for the hyperreals
Wed, 28 Jan 2004 10:41:49 +0100 paulson converted Real/Lubs to Isar script. Converting arithmetic setup
Tue, 27 Jan 2004 15:39:51 +0100 paulson replacing HOL/Real/PRat, PNat by the rational number development
Wed, 14 Jan 2004 04:41:16 +0100 nipkow fixed old bugs in "decomp" (conversion from term to lin.arith. format).
Wed, 14 Jan 2004 00:13:04 +0100 nipkow Told linear arithmetic package about injections "real" from nat/int into real.
Mon, 12 Jan 2004 16:45:35 +0100 paulson Modified real arithmetic simplification
Sat, 03 Jan 2004 16:09:39 +0100 paulson Deleting more redundant theorems
Thu, 01 Jan 2004 10:06:32 +0100 paulson tweaking of lemmas in RealDef, RealOrd
Tue, 23 Dec 2003 14:46:08 +0100 paulson new theorems
Tue, 23 Dec 2003 12:54:15 +0100 paulson more ML bindings
Mon, 22 Dec 2003 15:41:25 +0100 paulson new binding
Mon, 22 Dec 2003 12:50:01 +0100 paulson removing obsolete bindings
Fri, 19 Dec 2003 17:13:28 +0100 paulson tidying first part of HyperArith0.ML, using generic lemmas
Fri, 12 Dec 2003 15:05:18 +0100 paulson moving some division theorems to Ring_and_Field
Wed, 10 Dec 2003 16:47:50 +0100 paulson combining Real/{RealArith0,real_arith}.ML
Wed, 10 Dec 2003 15:59:34 +0100 paulson Moving some theorems from Real/RealArith0.ML
Mon, 01 Jan 2001 11:52:04 +0100 paulson minor tidying of simprocs
Thu, 21 Dec 2000 18:57:12 +0100 nipkow rational linear arithmetic
Mon, 18 Dec 2000 14:59:05 +0100 nipkow moved mk_bin from Numerals to HOLogic
Fri, 01 Dec 2000 19:53:29 +0100 nipkow Linear arithmetic now copes with mixed nat/int formulae.
Tue, 25 Jul 2000 00:06:46 +0200 wenzelm rearranged setup of arithmetic procedures, avoiding global reference values;
less more (0) tip