src/HOL/Groups.thy
2011-09-08 huffman 2011-09-08 remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
2011-08-22 wenzelm 2011-08-22 special treatment of structure index 1 in Pure, including legacy warning;
2011-08-20 huffman 2011-08-20 move lemma add_eq_0_iff to Groups.thy
2011-04-06 wenzelm 2011-04-06 discontinued old-style Syntax.constrainC;
2011-04-06 wenzelm 2011-04-06 typed_print_translation: discontinued show_sorts argument;
2011-04-06 wenzelm 2011-04-06 moved unparse material to syntax_phases.ML;
2010-11-05 haftmann 2010-11-05 added class relation group_add < cancel_semigroup_add
2010-09-05 wenzelm 2010-09-05 turned show_sorts/show_types into proper configuration options;
2010-07-28 wenzelm 2010-07-28 use file names relative to master directory of theory source -- Proof General can now handle that due to the ThyLoad.add_path deception (cf. 3ceccd415145);
2010-07-19 haftmann 2010-07-19 keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup
2010-07-19 haftmann 2010-07-19 discontinued pretending that abel_cancel is logic-independent; cleaned up junk
2010-05-17 huffman 2010-05-17 declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
2010-04-26 haftmann 2010-04-26 dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
2010-04-25 haftmann 2010-04-25 field_simps as named theorems
2010-04-23 haftmann 2010-04-23 more localization; tuned proofs
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-03-18 blanchet 2010-03-18 now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-03-11 haftmann 2010-03-11 tuned monoid locales and prefix of sublocale interpretations
2010-03-10 haftmann 2010-03-10 added locales for monoids
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2010-02-25 wenzelm 2010-02-25 more antiquotations;
2010-02-22 haftmann 2010-02-22 distributed theory Algebras to theories Groups and Lattices
2010-02-19 haftmann 2010-02-19 moved remaning class operations from Algebras.thy to Groups.thy
2010-02-18 huffman 2010-02-18 get rid of many duplicate simp rule warnings
2010-02-10 haftmann 2010-02-10 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
2010-02-08 haftmann 2010-02-08 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields