src/HOL/OrderedGroup.thy
2006-11-08 wenzelm 2006-11-08 proper definition of add_zero_left/right;
2006-06-06 wenzelm 2006-06-06 tuned;
2006-05-01 paulson 2006-05-01 some facts about min, max and add, diff
2006-04-10 obua 2006-04-10 Moved stuff from Ring_and_Field to Matrix
2006-03-10 haftmann 2006-03-10 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
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-17 haftmann 2005-06-17 migrated theory headers to new format
2005-03-07 obua 2005-03-07 Cleaning up HOL/Matrix
2005-02-21 nipkow 2005-02-21 comprehensive cleanup, replacing sumr by setsum
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-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-30 paulson 2004-07-30 conversion of Integration and NSPrimes to Isar scripts
2004-06-29 kleing 2004-06-29 license change to BSD
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