src/HOL/Ring_and_Field.thy
2007-07-03 huffman 2007-07-03 instance pordered_comm_ring < pordered_ring
2007-06-30 obua 2007-06-30 added ordered_ring and ordered_semiring
2007-06-25 nipkow 2007-06-25 removed redundant lemmas
2007-06-24 nipkow 2007-06-24 tex problem fixed
2007-06-24 nipkow 2007-06-24 tuned and used field_simps
2007-06-23 nipkow 2007-06-23 tuned and renamed group_eq_simps and ring_eq_simps
2007-06-17 nipkow 2007-06-17 tuned laws for cancellation in divisions for fields.
2007-06-17 chaieb 2007-06-17 added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub
2007-06-16 nipkow 2007-06-16 The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no longer need class numeral_ring. This made a number of special simp-thms redundant.
2007-06-15 nipkow 2007-06-15 made divide_self a simp rule
2007-06-14 wenzelm 2007-06-14 tuned proofs: avoid implicit prems;
2007-06-11 nipkow 2007-06-11 hid constant "dom"
2007-05-24 obua 2007-05-24 Squared things out.
2007-05-22 huffman 2007-05-22 add missing instance declarations
2007-05-17 haftmann 2007-05-17 tuned
2007-05-17 huffman 2007-05-17 added classes ring_no_zero_divisors and dom (non-commutative version of idom); generalized several cancellation lemmas to use the new classes
2007-05-17 huffman 2007-05-17 instance division_ring < no_zero_divisors; clean up field instance proofs
2007-05-06 haftmann 2007-05-06 added auxiliary lemmas for proof tools
2007-03-29 haftmann 2007-03-29 dropped legacy ML bindings
2007-03-16 haftmann 2007-03-16 adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
2007-03-09 haftmann 2007-03-09 stepping towards uniform lattice theory development in HOL
2007-03-02 haftmann 2007-03-02 now using "class"
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