src/HOL/Ring_and_Field.thy
Tue, 16 Aug 2005 18:53:11 +0200 paulson more simprules now have names
Tue, 12 Jul 2005 17:56:03 +0200 avigad added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
Sat, 25 Jun 2005 16:06:17 +0200 nipkow Changes due to new abel_cancel.ML
Wed, 04 May 2005 10:42:43 +0200 nipkow fixed lin.arith
Tue, 19 Apr 2005 10:59:31 +0200 obua Removed mult_commute axiom from comm_semiring axclass.
Mon, 07 Mar 2005 18:19:55 +0100 obua Cleaning up HOL/Matrix
Tue, 01 Feb 2005 18:01:57 +0100 paulson the new subst tactic, by Lucas Dixon
Thu, 07 Oct 2004 15:42:30 +0200 paulson simplification tweaks for better arithmetic reasoning
Tue, 05 Oct 2004 15:30:50 +0200 paulson new simprules for abs and for things like a/b<1
Mon, 04 Oct 2004 15:28:03 +0200 paulson revised simprules for division
Fri, 10 Sep 2004 20:04:14 +0200 nipkow Added antisymmetry simproc
Fri, 03 Sep 2004 17:10:36 +0200 obua Matrix theory, linear programming
Wed, 18 Aug 2004 11:09:40 +0200 nipkow import -> imports
Mon, 16 Aug 2004 14:22:27 +0200 nipkow New theory header syntax.
Mon, 26 Jul 2004 17:34:52 +0200 paulson converting Hyperreal/Transcendental to Isar script
Tue, 29 Jun 2004 11:18:34 +0200 kleing license change to BSD
Mon, 14 Jun 2004 14:20:55 +0200 obua Further development of matrix theory
Fri, 21 May 2004 21:16:51 +0200 wenzelm removed duplicate thms;
Tue, 18 May 2004 10:01:44 +0200 obua Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
Tue, 11 May 2004 20:11:08 +0200 obua changes made due to new Ring_and_Field theory
Fri, 16 Apr 2004 20:33:16 +0200 nipkow Moved ring stuff from ex into Ring_and_Field.
Thu, 15 Apr 2004 14:17:45 +0200 nipkow Added ex/Exceptions.thy
Thu, 01 Apr 2004 10:54:32 +0200 paulson new type class abelian_group
Fri, 19 Mar 2004 10:48:22 +0100 paulson new thms
Thu, 04 Mar 2004 12:06:07 +0100 paulson new material from Avigad, and simplified treatment of division by 0
Mon, 01 Mar 2004 13:51:21 +0100 paulson new Ring_and_Field hierarchy, eliminating redundant axioms
Thu, 19 Feb 2004 15:57:34 +0100 ballarin Efficient, graph-based reasoner for linear and partial orders.
Sun, 15 Feb 2004 10:46:37 +0100 paulson Polymorphic treatment of binary arithmetic using axclasses
Thu, 05 Feb 2004 10:45:28 +0100 paulson tidying up, especially the Complex numbers
Thu, 29 Jan 2004 16:51:17 +0100 paulson simplifications in 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
Mon, 12 Jan 2004 16:51:45 +0100 paulson Added lemmas to Ring_and_Field with slightly modified simplification rules
Fri, 09 Jan 2004 10:46:18 +0100 paulson Defining the type class "ringpower" and deleting superseded theorems for
Tue, 06 Jan 2004 10:40:15 +0100 paulson Ring_and_Field now requires axiom add_left_imp_eq for semirings.
Thu, 01 Jan 2004 10:06:32 +0100 paulson tweaking of lemmas in RealDef, RealOrd
Sat, 27 Dec 2003 21:02:14 +0100 paulson re-organized numeric lemmas
Tue, 23 Dec 2003 14:46:08 +0100 paulson new theorems
Fri, 19 Dec 2003 17:13:28 +0100 paulson tidying first part of HyperArith0.ML, using generic lemmas
Mon, 15 Dec 2003 16:38:25 +0100 paulson more general lemmas for Ring_and_Field
Sat, 13 Dec 2003 09:33:52 +0100 paulson absolute value theorems moved to HOL/Ring_and_Field
Fri, 12 Dec 2003 15:05:18 +0100 paulson moving some division theorems to Ring_and_Field
Wed, 10 Dec 2003 15:59:34 +0100 paulson Moving some theorems from Real/RealArith0.ML
Sun, 07 Dec 2003 16:30:06 +0100 paulson re-organisation of Real/RealArith0.ML; more `Isar scripts
Fri, 05 Dec 2003 18:10:59 +0100 paulson more field division lemmas transferred from Real to Ring_and_Field
Thu, 04 Dec 2003 10:29:17 +0100 paulson Tidying of the integer development; towards removing the
Tue, 02 Dec 2003 11:48:15 +0100 paulson More re-organising of numerical theorems
Fri, 28 Nov 2003 12:09:37 +0100 paulson conversion of some Real theories to Isar scripts
Thu, 27 Nov 2003 10:47:55 +0100 paulson Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
Tue, 25 Nov 2003 10:37:03 +0100 paulson More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
Mon, 24 Nov 2003 15:33:07 +0100 paulson conversion of integers to use Ring_and_Field;
Fri, 21 Nov 2003 11:15:40 +0100 paulson HOL: installation of Ring_and_Field as the basis for Naturals and Reals
less more (0) tip