src/HOL/Groups.thy
Tue, 18 Oct 2016 18:48:53 +0200 haftmann suitable logical type class for abs, sgn
Thu, 15 Sep 2016 10:40:10 +0200 hoelzl add add_eq_0_iff_both_eq_0 and zero_eq_add_iff_both_eq_0 to simp set
Fri, 12 Aug 2016 17:53:55 +0200 wenzelm more symbols;
Tue, 02 Aug 2016 21:05:34 +0200 wenzelm misc tuning and modernization;
Tue, 12 Jul 2016 13:55:35 +0200 fleury sharing simp rules between ordered monoids and rings
Sat, 02 Jul 2016 08:41:05 +0200 haftmann abstract and concrete multiplicative groups
Mon, 20 Jun 2016 21:40:48 +0200 wenzelm misc tuning and modernization;
Sat, 11 Jun 2016 16:22:42 +0200 haftmann boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
Wed, 25 May 2016 11:49:40 +0200 wenzelm isabelle update_cartouches -c -t;
Sun, 13 Mar 2016 10:22:46 +0100 haftmann more theorems on orderings
Mon, 22 Feb 2016 14:37:56 +0000 paulson An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
Fri, 19 Feb 2016 13:40:50 +0100 hoelzl generalize more theorems to support enat and ennreal
Fri, 12 Feb 2016 16:09:07 +0100 hoelzl moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
Wed, 10 Feb 2016 18:43:19 +0100 hoelzl Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
Wed, 17 Feb 2016 21:51:57 +0100 haftmann dropped various legacy fact bindings
Wed, 17 Feb 2016 21:51:57 +0100 haftmann generalized some lemmas;
Mon, 28 Dec 2015 01:26:34 +0100 wenzelm prefer symbols for "abs";
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Tue, 01 Dec 2015 14:09:10 +0000 paulson Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
Mon, 09 Nov 2015 15:48:17 +0100 wenzelm qualifier is mandatory by default;
Fri, 09 Oct 2015 20:26:03 +0200 wenzelm discontinued specific HTML syntax;
Tue, 06 Oct 2015 15:14:28 +0200 wenzelm fewer aliases for toplevel theorem statements;
Sun, 13 Sep 2015 22:56:52 +0200 wenzelm tuned proofs -- less legacy;
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
Mon, 20 Jul 2015 23:12:50 +0100 paulson new material for multivariate analysis, etc.
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Mon, 23 Mar 2015 19:05:14 +0100 haftmann explicit commutative additive inverse operation;
Thu, 19 Feb 2015 16:32:53 +0100 haftmann more canonical order of subscriptions avoids superfluous facts
Thu, 19 Feb 2015 11:53:36 +0100 haftmann establish unique preferred fact names
Thu, 08 Jan 2015 18:23:29 +0100 haftmann tuned order
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Sat, 16 Aug 2014 14:12:39 +0200 wenzelm updated to named_theorems;
Fri, 18 Jul 2014 14:21:42 +0200 nipkow reinstated popular add_ac and mult_ac to avoid needless incompatibilities in user space
Sat, 05 Jul 2014 11:01:53 +0200 haftmann prefer ac_simps collections over separate name bindings for add and mult
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Tue, 13 May 2014 11:35:51 +0200 hoelzl add mono rules for diff
Fri, 27 Dec 2013 14:35:14 +0100 haftmann prefer target-style syntaxx for sublocale
Mon, 09 Dec 2013 12:22:23 +0100 wenzelm more antiquotations;
Mon, 04 Nov 2013 20:10:09 +0100 haftmann fact generalization and name consolidation
Fri, 01 Nov 2013 18:51:14 +0100 haftmann more simplification rules on unary and binary minus
Fri, 18 Oct 2013 10:43:21 +0200 blanchet killed more "no_atp"s
Fri, 18 Oct 2013 10:43:20 +0200 blanchet killed most "no_atp", to make Sledgehammer more complete
Sun, 23 Jun 2013 21:16:07 +0200 haftmann migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
Sun, 02 Jun 2013 20:44:55 +0200 haftmann type class for confined subtraction
Tue, 28 May 2013 16:29:11 +0200 wenzelm more explicit Printer.type_emphasis, depending on show_type_emphasis;
Sat, 25 May 2013 15:37:53 +0200 wenzelm syntax translations always depend on context;
Tue, 26 Mar 2013 21:53:56 +0100 haftmann more uniform style for interpretation and sublocale declarations
Wed, 03 Oct 2012 16:59:58 +0200 wenzelm more explicit show_type_constraint, show_sort_constraint;
Sat, 15 Sep 2012 20:14:29 +0200 haftmann typeclass formalising bounded subtraction
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Fri, 27 Jul 2012 15:42:39 +0200 huffman replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
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
less more (0) -60 tip