src/HOL/Groups.thy
Thu, 17 Nov 2011 18:31:00 +0100 huffman Groups.thy: generalize several lemmas from class ab_group_add to class group_add
Fri, 28 Oct 2011 23:41:16 +0200 wenzelm tuned Named_Thms: proper binding;
Thu, 08 Sep 2011 18:47:23 -0700 huffman remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
Mon, 22 Aug 2011 23:39:05 +0200 wenzelm special treatment of structure index 1 in Pure, including legacy warning;
Sat, 20 Aug 2011 13:07:00 -0700 huffman move lemma add_eq_0_iff to Groups.thy
Wed, 06 Apr 2011 14:08:40 +0200 wenzelm discontinued old-style Syntax.constrainC;
Wed, 06 Apr 2011 13:33:46 +0200 wenzelm typed_print_translation: discontinued show_sorts argument;
Wed, 06 Apr 2011 12:58:13 +0200 wenzelm moved unparse material to syntax_phases.ML;
Fri, 05 Nov 2010 14:10:41 +0100 haftmann added class relation group_add < cancel_semigroup_add
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