src/HOL/Finite_Set.thy
2010-03-10 haftmann 2010-03-10 split off theory Big_Operators from theory Finite_Set
2010-03-04 hoelzl 2010-03-04 Generalized setsum_cases
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-19 haftmann 2010-02-19 moved remaning class operations from Algebras.thy to Groups.thy
2010-02-18 huffman 2010-02-18 get rid of many duplicate simp rule warnings
2010-02-17 hoelzl 2010-02-17 Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
2010-02-08 haftmann 2010-02-08 added lemmas involving Min, Max, uminus
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-01-01 nipkow 2010-01-01 added lemmas
2009-12-17 huffman 2009-12-17 merged
2009-12-17 huffman 2009-12-17 add lemmas rev_finite_subset, finite_vimageD, finite_vimage_iff
2009-12-17 paulson 2009-12-17 Two new theorems about cardinality
2009-12-05 haftmann 2009-12-05 tuned lattices theory fragements; generlized some lemmas from sets to lattices
2009-11-25 haftmann 2009-11-25 tuned
2009-11-13 nipkow 2009-11-13 renamed lemmas "anti_sym" -> "antisym"
2009-11-04 nipkow 2009-11-04 fixed order of parameters in induction rules
2009-10-22 nipkow 2009-10-22 inv_onto -> inv_into
2009-10-18 nipkow 2009-10-18 merged
2009-10-18 nipkow 2009-10-18 Inv -> inv_onto, inv abbr. inv_onto UNIV.
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-09-25 haftmann 2009-09-25 merged
2009-09-23 haftmann 2009-09-23 inf/sup_absorb are no default simp rules any longer
2009-09-22 haftmann 2009-09-22 merged
2009-09-19 haftmann 2009-09-19 inter and union are mere abbreviations for inf and sup
2009-09-24 haftmann 2009-09-24 idempotency case for fold1
2009-09-22 haftmann 2009-09-22 be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
2009-08-28 nipkow 2009-08-28 tuned proofs
2009-07-25 haftmann 2009-07-25 adapted to localized interpretation of min/max-lattice
2009-07-20 haftmann 2009-07-20 merged
2009-07-14 haftmann 2009-07-14 refinement of lattice classes
2009-07-15 nipkow 2009-07-15 More finite set induction rules
2009-07-12 nipkow 2009-07-12 typo
2009-07-12 nipkow 2009-07-12 resolvd conflict
2009-07-12 nipkow 2009-07-12 More about gcd/lcm, and some cleaning up
2009-07-11 haftmann 2009-07-11 added boolean_algebra type class; tuned lattice duals
2009-07-02 wenzelm 2009-07-02 recovered subscripts, which were lost in b41d61c768e2 (due to Emacs accident?);
2009-06-23 paulson 2009-06-23 merged
2009-06-18 paulson 2009-06-18 Removed unnecessary conditions concerning nonzero divisors
2009-06-23 haftmann 2009-06-23 lemma finite_image_set by Jeremy Avigad
2009-06-05 haftmann 2009-06-05 merged
2009-06-05 haftmann 2009-06-05 merged
2009-06-04 haftmann 2009-06-04 lemmas about basic set operations and Finite_Set.fold
2009-06-05 nipkow 2009-06-05 new lemma
2009-06-04 nipkow 2009-06-04 finite lemmas
2009-06-04 nipkow 2009-06-04 A few finite lemmas
2009-06-02 haftmann 2009-06-02 added/moved lemmas by Andreas Lochbihler
2009-05-09 nipkow 2009-05-09 lemmas by Andreas Lochbihler
2009-04-28 haftmann 2009-04-28 stripped class recpower further
2009-04-03 nipkow 2009-04-03 Finite_Set: lemma IsarRef: attribute arith
2009-04-03 nipkow 2009-04-03 added setsum_eq_1_iff
2009-04-01 nipkow 2009-04-01 merged
2009-04-01 nipkow 2009-04-01 cleaned up setprod_zero-related lemmas
2009-04-01 huffman 2009-04-01 merged
2009-04-01 huffman 2009-04-01 generalized setprod_nonneg and setprod_pos to ordered_semidom, simplified proofs
2009-04-01 nipkow 2009-04-01 added strong_setprod_cong[cong] (in analogy with setsum) added some lemmas
2009-03-26 wenzelm 2009-03-26 interpretation/interpret: prefixes are mandatory by default;
2009-03-06 haftmann 2009-03-06 equalities for Min, Max
2009-03-04 chaieb 2009-03-04 Added general theorems for fold_image, setsum and set_prod
2009-02-18 haftmann 2009-02-18 reverted to previous version of Finite_Set.thy