src/HOL/Groups.thy
Thu, 11 Mar 2021 07:05:38 +0000 haftmann avoid name clash
Fri, 10 Apr 2020 22:50:59 +0100 paulson more removal of applys
Sun, 09 Feb 2020 21:58:42 +0000 haftmann more rules for natural deduction from inequalities
Sat, 09 Nov 2019 10:38:51 +0000 haftmann new lemma
Wed, 09 Oct 2019 14:51:54 +0000 haftmann dedicated fact collections for algebraic simplification rules potentially splitting goals
Thu, 08 Aug 2019 12:11:40 +0200 wenzelm prefer named lemmas -- more compact proofterms;
Fri, 14 Jun 2019 08:34:28 +0000 haftmann official fact collection sign_simps
Sun, 06 Jan 2019 15:04:34 +0100 wenzelm isabelle update -u path_cartouches;
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Wed, 31 Oct 2018 15:53:32 +0100 wenzelm clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
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;
less more (0) -60 tip