src/HOL/Groups_Big.thy
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