src/HOL/Real/rat_arith.ML
Tue, 31 Jul 2007 19:40:24 +0200 wenzelm tuned LinArith setup;
Tue, 12 Jun 2007 21:59:40 +0200 huffman thm antiquotations
Wed, 23 May 2007 02:50:19 +0200 huffman remove unused simproc definition
Wed, 23 May 2007 01:46:15 +0200 huffman remove redundant simproc
Thu, 26 Apr 2007 13:33:09 +0200 haftmann slightly tuned
Thu, 29 Mar 2007 14:21:45 +0200 haftmann dropped legacy ML bindings
Wed, 08 Nov 2006 13:48:29 +0100 wenzelm removed theory NatArith (now part of Nat);
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;
Wed, 04 May 2005 10:42:43 +0200 nipkow fixed lin.arith
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.
Fri, 06 Aug 2004 17:07:04 +0200 nipkow Initial changes to extend arithmetic from individual types to type classes.
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
Tue, 10 Feb 2004 12:02:11 +0100 paulson generic of_nat and of_int functions, and generalization of iszero
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
less more (0) tip