src/HOL/Ring_and_Field.thy
2006-11-13 haftmann 2006-11-13 dropped Inductive dependency
2006-11-09 huffman 2006-11-09 added lemma mult_mono'
2006-11-07 krauss 2006-11-07 * Added annihilation axioms ("x * 0 = 0") to axclass semiring_0. Richer structures do not inherit from semiring_0 anymore, because anihilation is a theorem there, not an axiom. * Generalized axclass "recpower" to arbitrary monoid, not just commutative semirings.
2006-09-20 wenzelm 2006-09-20 renamed axclass_xxxx axclasses;
2006-09-19 obua 2006-09-19 renamed axclass_xxxx axclasses
2006-09-10 huffman 2006-09-10 added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
2006-04-10 obua 2006-04-10 Moved stuff from Ring_and_Field to Matrix
2006-01-11 paulson 2006-01-11 tidied, and added missing thm divide_less_eq_1_neg
2006-01-09 paulson 2006-01-09 simplified the special-case simprules
2005-08-16 paulson 2005-08-16 more simprules now have names
2005-07-12 avigad 2005-07-12 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities) added lemmas to Ring_and_Field.thy (reasoning about signs, fractions, etc.) renamed simplification rules for abs (abs_of_pos, etc.) renamed rules for multiplication and signs (mult_pos_pos, etc.) moved lemmas involving fractions from NatSimprocs.thy added setsum_mono3 to FiniteSet.thy added simplification rules for powers to Parity.thy
2005-06-25 nipkow 2005-06-25 Changes due to new abel_cancel.ML
2005-05-04 nipkow 2005-05-04 fixed lin.arith
2005-04-19 obua 2005-04-19 Removed mult_commute axiom from comm_semiring axclass.
2005-03-07 obua 2005-03-07 Cleaning up HOL/Matrix
2005-02-01 paulson 2005-02-01 the new subst tactic, by Lucas Dixon
2004-10-07 paulson 2004-10-07 simplification tweaks for better arithmetic reasoning
2004-10-05 paulson 2004-10-05 new simprules for abs and for things like a/b<1
2004-10-04 paulson 2004-10-04 revised simprules for division
2004-09-10 nipkow 2004-09-10 Added antisymmetry simproc
2004-09-03 obua 2004-09-03 Matrix theory, linear programming
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-07-26 paulson 2004-07-26 converting Hyperreal/Transcendental to Isar script
2004-06-29 kleing 2004-06-29 license change to BSD
2004-06-14 obua 2004-06-14 Further development of matrix theory
2004-05-21 wenzelm 2004-05-21 removed duplicate thms;
2004-05-18 obua 2004-05-18 Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
2004-05-11 obua 2004-05-11 changes made due to new Ring_and_Field theory
2004-04-16 nipkow 2004-04-16 Moved ring stuff from ex into Ring_and_Field.
2004-04-15 nipkow 2004-04-15 Added ex/Exceptions.thy
2004-04-01 paulson 2004-04-01 new type class abelian_group
2004-03-19 paulson 2004-03-19 new thms
2004-03-04 paulson 2004-03-04 new material from Avigad, and simplified treatment of division by 0
2004-03-01 paulson 2004-03-01 new Ring_and_Field hierarchy, eliminating redundant axioms
2004-02-19 ballarin 2004-02-19 Efficient, graph-based reasoner for linear and partial orders. + Setup as solver in the HOL simplifier.
2004-02-15 paulson 2004-02-15 Polymorphic treatment of binary arithmetic using axclasses
2004-02-05 paulson 2004-02-05 tidying up, especially the Complex numbers
2004-01-29 paulson 2004-01-29 simplifications in the hyperreals
2004-01-28 paulson 2004-01-28 converted Real/Lubs to Isar script. Converting arithmetic setup files to be polymorphic.
2004-01-27 paulson 2004-01-27 replacing HOL/Real/PRat, PNat by the rational number development of Markus Wenzel
2004-01-12 paulson 2004-01-12 Added lemmas to Ring_and_Field with slightly modified simplification rules Deleted some little-used integer theorems, replacing them by the generic ones in Ring_and_Field Consolidated integer powers
2004-01-09 paulson 2004-01-09 Defining the type class "ringpower" and deleting superseded theorems for types nat, int, real, hypreal
2004-01-06 paulson 2004-01-06 Ring_and_Field now requires axiom add_left_imp_eq for semirings. This allows more theorems to be proved for semirings, but requires a redundant axiom to be proved for rings, etc.
2004-01-01 paulson 2004-01-01 tweaking of lemmas in RealDef, RealOrd
2003-12-27 paulson 2003-12-27 re-organized numeric lemmas
2003-12-23 paulson 2003-12-23 new theorems
2003-12-19 paulson 2003-12-19 tidying first part of HyperArith0.ML, using generic lemmas
2003-12-15 paulson 2003-12-15 more general lemmas for Ring_and_Field
2003-12-13 paulson 2003-12-13 absolute value theorems moved to HOL/Ring_and_Field
2003-12-12 paulson 2003-12-12 moving some division theorems to Ring_and_Field
2003-12-10 paulson 2003-12-10 Moving some theorems from Real/RealArith0.ML
2003-12-07 paulson 2003-12-07 re-organisation of Real/RealArith0.ML; more `Isar scripts
2003-12-05 paulson 2003-12-05 more field division lemmas transferred from Real to Ring_and_Field
2003-12-04 paulson 2003-12-04 Tidying of the integer development; towards removing the abel_cancel simproc
2003-12-02 paulson 2003-12-02 More re-organising of numerical theorems
2003-11-28 paulson 2003-11-28 conversion of some Real theories to Isar scripts
2003-11-27 paulson 2003-11-27 Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files. New theorems for Ring_and_Field. Fixing affected proofs.
2003-11-25 paulson 2003-11-25 More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas to Isar script.
2003-11-24 paulson 2003-11-24 conversion of integers to use Ring_and_Field; new lemmas for Ring_and_Field