src/HOL/Finite_Set.thy
2011-07-17 haftmann 2011-07-17 moving UNIV = ... equations to their proper theories
2011-05-20 haftmann 2011-05-20 tuned proofs
2011-05-20 haftmann 2011-05-20 point-free characterization of operations on finite sets
2011-05-20 haftmann 2011-05-20 names of fold_set locales resemble name of characteristic property more closely
2011-05-20 haftmann 2011-05-20 use point-free characterization for locale fun_left_comm_idem
2011-05-14 haftmann 2011-05-14 use pointfree characterisation for fold_set locale
2011-05-12 haftmann 2011-05-12 more uniform naming of lemma
2011-04-07 haftmann 2011-04-07 dropped unused lemmas; proper Isar proof
2011-04-03 haftmann 2011-04-03 tuned proofs
2011-04-02 haftmann 2011-04-02 tuned proof
2011-03-17 nipkow 2011-03-17 tuned lemma
2011-03-16 nipkow 2011-03-16 added lemmas
2011-01-21 haftmann 2011-01-21 moved theorem
2011-01-21 haftmann 2011-01-21 restructured theory; tuned proofs
2011-01-14 wenzelm 2011-01-14 eliminated global prems; tuned proofs;
2010-12-03 wenzelm 2010-12-03 recoded latin1 as utf8; use textcomp for some text symbols where it appears appropriate;
2010-12-03 bulwahn 2010-12-03 adding code equation for finiteness of finite types
2010-11-28 nipkow 2010-11-28 gave more standard finite set rules simp and intro attribute
2010-11-26 nipkow 2010-11-26 new lemma
2010-11-23 hoelzl 2010-11-23 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
2010-11-22 hoelzl 2010-11-22 Replace surj by abbreviation; remove surj_on.
2010-11-03 nipkow 2010-11-03 removed assumption
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-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;