src/HOL/Groups_Big.thy
22 months ago haftmann 2017-10-08 avoid name clashes on interpretation of abstract locales
2017-08-07 blanchet 2017-08-07 tuning imports
2017-06-19 paulson 2017-06-19 New theorems; stronger theorems; tidier theorems. Also some renaming
2017-06-15 paulson 2017-06-15 Some new material. SIMPRULE STATUS for sum/prod.delta rules!
2017-05-03 paulson 2017-05-03 two new theorems
2017-05-02 paulson 2017-05-02 Simplification of some proofs. Also key lemmas using !! rather than ! in premises
2017-02-02 hoelzl 2017-02-02 move mono_neutral_cong from AFP/Deep_Learning/PP_Auxiliary
2016-10-17 nipkow 2016-10-17 setprod -> prod
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-09-28 paulson 2016-09-28 new material connected with HOL Light measure theory, plus more rationalisation
2016-09-22 paulson 2016-09-22 More mainly topological results
2016-09-18 haftmann 2016-09-18 more generic algebraic lemmas
2016-09-19 fleury 2016-09-19 left_distrib ~> distrib_right, right_distrib ~> distrib_left
2016-09-18 wenzelm 2016-09-18 tuned proofs;
2016-08-10 wenzelm 2016-08-10 misc tuning and modernization;
2016-07-29 Andreas Lochbihler 2016-07-29 add lemmas contributed by Peter Gammie
2016-06-26 nipkow 2016-06-26 added fundef_cong rule
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-13 wenzelm 2016-05-13 eliminated use of empty "assms";
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-03-01 haftmann 2016-03-01 tuned bootstrap order to provide type classes in a more sensible order
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.
2015-12-28 wenzelm 2015-12-28 former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
2015-12-28 wenzelm 2015-12-28 prefer symbols for "Union", "Inter";
2015-12-28 wenzelm 2015-12-28 prefer symbols for "abs";
2015-12-27 wenzelm 2015-12-27 discontinued ASCII replacement syntax <*>;
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-12-02 haftmann 2015-12-02 modernized
2015-11-09 wenzelm 2015-11-09 qualifier is mandatory by default;
2015-11-04 ballarin 2015-11-04 Keyword 'rewrites' identifies rewrite morphisms.
2015-10-29 eberlm 2015-10-29 added many small lemmas about setsum/setprod/powr/...
2015-10-09 wenzelm 2015-10-09 discontinued specific HTML syntax;
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-08-27 haftmann 2015-08-27 standardized some occurences of ancient "split" alias
2015-08-19 paulson 2015-08-19 New material and fixes related to the forthcoming Stone-Weierstrass development
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-06-17 paulson 2015-06-17 correccted the pretty-printing specs for setsum and setprod
2015-06-12 haftmann 2015-06-12 uniform _ div _ as infix syntax for ring division
2015-06-01 haftmann 2015-06-01 implicit partial divison operation in integral domains
2015-03-31 haftmann 2015-03-31 given up separate type classes demanding `inverse 0 = 0`
2015-03-28 haftmann 2015-03-28 clarified no_zero_devisors: makes only sense in a semiring; actually turn linorder_semidom into a integral domain
2015-03-06 paulson 2015-03-06 A few new lemmas and a bit of tidying up
2015-01-20 hoelzl 2015-01-20 generalized sum_diff_distrib to setsum_subtractf_nat
2014-11-17 haftmann 2014-11-17 generalized lemmas and tuned proofs
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-24 haftmann 2014-09-24 added lemmas
2014-09-16 nipkow 2014-09-16 added lemma
2014-09-06 haftmann 2014-09-06 added various facts
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-06-18 hoelzl 2014-06-18 moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
2014-05-30 hoelzl 2014-05-30 introduce more powerful reindexing rules for big operators
2014-04-12 haftmann 2014-04-12 more operations and lemmas
2014-04-12 nipkow 2014-04-12 made mult_pos_pos a simp rule
2014-04-11 nipkow 2014-04-11 made mult_nonneg_nonneg a simp rule
2014-03-16 haftmann 2014-03-16 normalising simp rules for compound operators
2014-01-21 traytel 2014-01-21 removed theory dependency of BNF_LFP on Datatype
2013-12-15 haftmann 2013-12-15 disambiguation of interpretation prefixes