src/HOL/Finite_Set.thy
2010-08-13 haftmann 2010-08-13 import swap prevents strange failure of SML code generator for datatypes
2010-07-12 haftmann 2010-07-12 avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-06-18 nipkow 2010-06-18 added pigeonhole lemmas
2010-05-04 haftmann 2010-05-04 avoid if on rhs of default simp rules
2010-05-04 haftmann 2010-05-04 locale predicates of classes carry a mandatory "class" prefix
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
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-30 huffman 2010-03-30 simplify fold_graph proofs
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 added locales folding_one_(idem); various streamlining and tuning
2010-03-15 haftmann 2010-03-15 corrected disastrous syntax declarations
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
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