src/HOL/Groups.thy
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