src/HOL/Big_Operators.thy
2011-09-09 krauss 2011-09-09 added syntactic classes for "inf" and "sup"
2011-05-26 hoelzl 2011-05-26 generalize setsum_cases
2011-05-20 haftmann 2011-05-20 names of fold_set locales resemble name of characteristic property more closely
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-01-14 wenzelm 2011-01-14 eliminated global prems; tuned proofs;
2010-11-28 nipkow 2010-11-28 gave more standard finite set rules simp and intro attribute
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-05-17 huffman 2010-05-17 declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
2010-05-04 haftmann 2010-05-04 locale predicates of classes carry a mandatory "class" prefix
2010-04-20 hoelzl 2010-04-20 Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
2010-04-26 haftmann 2010-04-26 use new classes (linordered_)field_inverse_zero
2010-04-26 haftmann 2010-04-26 class division_ring_inverse_zero
2010-04-23 haftmann 2010-04-23 sharpened constraint (c.f. 4e7f5b22dd7d)
2010-04-07 Christian Urban 2010-04-07 simplified induction case in finite_psubset_induct; tuned the proof that uses this induction principle
2010-03-23 huffman 2010-03-23 sublocale comm_monoid_add < setprod --> sublocale comm_monoid_mult < setprod
2010-03-18 blanchet 2010-03-18 merged
2010-03-18 blanchet 2010-03-18 now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-03-18 haftmann 2010-03-18 generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
2010-03-11 haftmann 2010-03-11 moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
2010-03-10 haftmann 2010-03-10 split off theory Big_Operators from theory Finite_Set