src/HOL/Groups.thy
2016-07-12 fleury 2016-07-12 sharing simp rules between ordered monoids and rings
2016-07-02 haftmann 2016-07-02 abstract and concrete multiplicative groups
2016-06-20 wenzelm 2016-06-20 misc tuning and modernization;
2016-06-11 haftmann 2016-06-11 boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
2016-05-25 wenzelm 2016-05-25 isabelle update_cartouches -c -t;
2016-03-13 haftmann 2016-03-13 more theorems on orderings
2016-02-22 paulson 2016-02-22 An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
2016-02-19 hoelzl 2016-02-19 generalize more theorems to support enat and ennreal
2016-02-12 hoelzl 2016-02-12 moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
2016-02-10 hoelzl 2016-02-10 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.
2016-02-17 haftmann 2016-02-17 dropped various legacy fact bindings
2016-02-17 haftmann 2016-02-17 generalized some lemmas; moved some lemmas in more appropriate places; deleted potentially dangerous simp rule
2015-12-28 wenzelm 2015-12-28 prefer symbols for "abs";
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-12-01 paulson 2015-12-01 Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
2015-11-09 wenzelm 2015-11-09 qualifier is mandatory by default;
2015-10-09 wenzelm 2015-10-09 discontinued specific HTML syntax;
2015-10-06 wenzelm 2015-10-06 fewer aliases for toplevel theorem statements;
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-07-20 paulson 2015-07-20 new material for multivariate analysis, etc.
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-03-23 haftmann 2015-03-23 explicit commutative additive inverse operation; more explicit focal point for commutative monoids with an inverse operation
2015-02-19 haftmann 2015-02-19 more canonical order of subscriptions avoids superfluous facts
2015-02-19 haftmann 2015-02-19 establish unique preferred fact names
2015-01-08 haftmann 2015-01-08 tuned order
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-08-16 wenzelm 2014-08-16 updated to named_theorems;
2014-07-18 nipkow 2014-07-18 reinstated popular add_ac and mult_ac to avoid needless incompatibilities in user space
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-05-13 hoelzl 2014-05-13 add mono rules for diff
2013-12-27 haftmann 2013-12-27 prefer target-style syntaxx for sublocale
2013-12-09 wenzelm 2013-12-09 more antiquotations;
2013-11-04 haftmann 2013-11-04 fact generalization and name consolidation
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-10-18 blanchet 2013-10-18 killed more "no_atp"s
2013-10-18 blanchet 2013-10-18 killed most "no_atp", to make Sledgehammer more complete
2013-06-23 haftmann 2013-06-23 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2013-06-02 haftmann 2013-06-02 type class for confined subtraction
2013-05-28 wenzelm 2013-05-28 more explicit Printer.type_emphasis, depending on show_type_emphasis; tuned signature;
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
2013-03-26 haftmann 2013-03-26 more uniform style for interpretation and sublocale declarations
2012-10-03 wenzelm 2012-10-03 more explicit show_type_constraint, show_sort_constraint;
2012-09-15 haftmann 2012-09-15 typeclass formalising bounded subtraction
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-07-27 huffman 2012-07-27 replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
2011-11-17 huffman 2011-11-17 Groups.thy: generalize several lemmas from class ab_group_add to class group_add
2011-10-28 wenzelm 2011-10-28 tuned Named_Thms: proper binding;
2011-09-08 huffman 2011-09-08 remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
2011-08-22 wenzelm 2011-08-22 special treatment of structure index 1 in Pure, including legacy warning;
2011-08-20 huffman 2011-08-20 move lemma add_eq_0_iff to Groups.thy
2011-04-06 wenzelm 2011-04-06 discontinued old-style Syntax.constrainC;
2011-04-06 wenzelm 2011-04-06 typed_print_translation: discontinued show_sorts argument;
2011-04-06 wenzelm 2011-04-06 moved unparse material to syntax_phases.ML;
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