src/HOL/Ring_and_Field.thy
Sun, 24 Jun 2007 21:15:55 +0200 nipkow tex problem fixed
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
Sun, 17 Jun 2007 18:47:03 +0200 nipkow tuned laws for cancellation in divisions for fields.
Sun, 17 Jun 2007 13:39:29 +0200 chaieb added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub
Sat, 16 Jun 2007 15:01:54 +0200 nipkow The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
Fri, 15 Jun 2007 15:10:32 +0200 nipkow made divide_self a simp rule
Thu, 14 Jun 2007 18:33:31 +0200 wenzelm tuned proofs: avoid implicit prems;
Mon, 11 Jun 2007 16:21:03 +0200 nipkow hid constant "dom"
Thu, 24 May 2007 16:52:54 +0200 obua Squared things out.
Tue, 22 May 2007 16:47:22 +0200 huffman add missing instance declarations
Thu, 17 May 2007 19:49:16 +0200 haftmann tuned
Thu, 17 May 2007 18:32:17 +0200 huffman added classes ring_no_zero_divisors and dom (non-commutative version of idom);
Thu, 17 May 2007 08:42:51 +0200 huffman instance division_ring < no_zero_divisors; clean up field instance proofs
Sun, 06 May 2007 21:49:29 +0200 haftmann added auxiliary lemmas for proof tools
Thu, 29 Mar 2007 14:21:45 +0200 haftmann dropped legacy ML bindings
Fri, 16 Mar 2007 21:32:08 +0100 haftmann adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
Fri, 09 Mar 2007 08:45:50 +0100 haftmann stepping towards uniform lattice theory development in HOL
Fri, 02 Mar 2007 15:43:21 +0100 haftmann now using "class"
Mon, 13 Nov 2006 15:43:05 +0100 haftmann dropped Inductive dependency
Thu, 09 Nov 2006 00:43:12 +0100 huffman added lemma mult_mono'
Tue, 07 Nov 2006 09:33:47 +0100 krauss * Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
Wed, 20 Sep 2006 00:24:24 +0200 wenzelm renamed axclass_xxxx axclasses;
Tue, 19 Sep 2006 18:13:10 +0200 obua renamed axclass_xxxx axclasses
Sun, 10 Sep 2006 05:34:24 +0200 huffman added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
Mon, 10 Apr 2006 16:00:34 +0200 obua Moved stuff from Ring_and_Field to Matrix
Wed, 11 Jan 2006 11:00:26 +0100 paulson tidied, and added missing thm divide_less_eq_1_neg
Mon, 09 Jan 2006 13:28:06 +0100 paulson simplified the special-case simprules
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
less more (0) -60 tip