src/HOL/Groups.thy
Sun, 05 Sep 2010 21:41:24 +0200 wenzelm turned show_sorts/show_types into proper configuration options;
Wed, 28 Jul 2010 00:03:22 +0200 wenzelm 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);
Mon, 19 Jul 2010 20:23:49 +0200 haftmann keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup
Mon, 19 Jul 2010 16:09:43 +0200 haftmann discontinued pretending that abel_cancel is logic-independent; cleaned up junk
Mon, 17 May 2010 18:59:59 -0700 huffman declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
Mon, 26 Apr 2010 11:34:15 +0200 haftmann dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
Sun, 25 Apr 2010 08:25:34 +0200 haftmann field_simps as named theorems
Fri, 23 Apr 2010 13:58:15 +0200 haftmann more localization; tuned proofs
Fri, 16 Apr 2010 21:28:09 +0200 wenzelm replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
Thu, 18 Mar 2010 12:58:52 +0100 blanchet now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
Thu, 11 Mar 2010 14:38:19 +0100 haftmann tuned monoid locales and prefix of sublocale interpretations
Wed, 10 Mar 2010 16:53:43 +0100 haftmann added locales for monoids
Sat, 27 Feb 2010 23:13:01 +0100 wenzelm modernized structure Term_Ord;
Thu, 25 Feb 2010 22:32:09 +0100 wenzelm more antiquotations;
Mon, 22 Feb 2010 15:53:18 +0100 haftmann distributed theory Algebras to theories Groups and Lattices
Fri, 19 Feb 2010 14:47:01 +0100 haftmann moved remaning class operations from Algebras.thy to Groups.thy
Thu, 18 Feb 2010 14:21:44 -0800 huffman get rid of many duplicate simp rule warnings
Wed, 10 Feb 2010 14:12:04 +0100 haftmann moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
Mon, 08 Feb 2010 17:12:38 +0100 haftmann renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
less more (0) tip