src/HOL/OrderedGroup.thy
2009-02-14 huffman 2009-02-14 generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
2009-02-13 huffman 2009-02-13 add class cancel_comm_monoid_add
2009-02-12 huffman 2009-02-12 add lemma add_nonneg_eq_0_iff
2009-02-08 nipkow 2009-02-08 added noatps
2009-01-28 nipkow 2009-01-28 removed spurious conflic msg
2009-01-28 nipkow 2009-01-28 merged - resolving conflics
2009-01-28 nipkow 2009-01-28 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
2009-01-19 haftmann 2009-01-19 tuned proof
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2008-11-17 haftmann 2008-11-17 tuned unfold_locales invocation
2008-09-17 wenzelm 2008-09-17 back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
2008-09-04 huffman 2008-09-04 move diff_add_cancel, add_diff_cancel from class ab_group_add to group_add
2008-07-10 huffman 2008-07-10 by intro_locales -> ..
2008-07-03 huffman 2008-07-03 move proofs of add_left_cancel and add_right_cancel into the correct locale
2008-06-18 wenzelm 2008-06-18 simplified Abel_Cancel setup;
2008-03-29 wenzelm 2008-03-29 replaced 'ML_setup' by 'ML';
2008-02-15 haftmann 2008-02-15 moved *_reorient lemmas here
2008-01-30 haftmann 2008-01-30 idempotent semigroups
2008-01-02 haftmann 2008-01-02 splitted class uminus from class minus
2007-12-13 haftmann 2007-12-13 dropped ws
2007-11-30 haftmann 2007-11-30 using intro_locales instead of unfold_locales if appropriate
2007-11-06 haftmann 2007-11-06 simplified specification of *_abs class
2007-11-06 haftmann 2007-11-06 renamed lordered_*_* to lordered_*_add_*; further localization
2007-11-02 haftmann 2007-11-02 proper reinitialisation after subclass
2007-10-30 haftmann 2007-10-30 continued localization
2007-10-25 haftmann 2007-10-25 dropped redundancy
2007-10-19 haftmann 2007-10-19 antisymmetry not a default intro rule any longer
2007-10-19 haftmann 2007-10-19 98% localized
2007-10-18 haftmann 2007-10-18 continued localization
2007-10-16 haftmann 2007-10-16 global class syntax
2007-09-29 haftmann 2007-09-29 proper syntax during class specification
2007-08-21 haftmann 2007-08-21 moved ordered_ab_semigroup_add to OrderedGroup.thy
2007-08-15 paulson 2007-08-15 ATP blacklisting is now in theory data, attribute noatp
2007-08-03 wenzelm 2007-08-03 replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
2007-07-20 haftmann 2007-07-20 split class abs from class minus
2007-06-23 nipkow 2007-06-23 tuned and renamed group_eq_simps and ring_eq_simps
2007-06-14 wenzelm 2007-06-14 tuned proofs: avoid implicit prems;
2007-06-01 haftmann 2007-06-01 localized
2007-05-24 nipkow 2007-05-24 Introduced new classes monoid_add and group_add
2007-05-17 haftmann 2007-05-17 canonical prefixing of class constants
2007-05-17 huffman 2007-05-17 remove redundant instance declaration
2007-03-29 haftmann 2007-03-29 dropped legacy ML bindings
2007-03-20 haftmann 2007-03-20 dropped OrderedGroup.ML
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-15 haftmann 2006-11-15 dropped dependency on sets
2006-11-13 haftmann 2006-11-13 dropped Inductive dependency
2006-11-12 nipkow 2006-11-12 started reorgnization of lattice theories
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