src/HOL/Groups_Big.thy
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
2013-12-15 haftmann 2013-12-15 more algebraic terminology for theories about big operators