src/HOL/Finite_Set.thy
2013-03-23 haftmann 2013-03-23 fundamental revision of big operators on sets
2013-03-23 haftmann 2013-03-23 locales for abstract orders
2013-02-27 Andreas Lochbihler 2013-02-27 added lemma
2012-10-10 wenzelm 2012-10-10 merged
2012-10-10 bulwahn 2012-10-10 moving simproc from Finite_Set to more appropriate Product_Type theory
2012-10-09 kuncar 2012-10-09 use Set.filter instead of Finite_Set.filter, which is removed then
2012-10-09 kuncar 2012-10-09 rename Set.project to Set.filter - more appropriate name
2012-10-10 wenzelm 2012-10-10 added some ad-hoc namespace prefixes to avoid duplicate facts;
2012-10-08 haftmann 2012-10-08 consolidated names of theorems on composition; generalized former theorem UN_o; comp_assoc orients to the right, as is more common
2012-10-06 haftmann 2012-10-06 congruence rule for Finite_Set.fold
2012-10-06 haftmann 2012-10-06 alternative simplification of ^^ to the righthand side; lifting of comp_fun_commute to ^^
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-08-01 wenzelm 2012-08-01 removed junk;
2012-07-31 kuncar 2012-07-31 more set operations expressed by Finite_Set.fold
2012-07-03 Andreas Lochbihler 2012-07-03 add finiteness lemmas for 'a * 'b and 'a set
2012-06-25 wenzelm 2012-06-25 merged, resolving conflict with 87c831e30f0a;
2012-06-25 wenzelm 2012-06-25 tuned proofs -- prefer direct "rotated" instead of old-style COMP;
2012-06-25 wenzelm 2012-06-25 ignore morphism more explicitly; tuned headers;
2012-06-25 bulwahn 2012-06-25 adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions; noting further steps with FIXME
2012-06-20 Rafal Kolanski 2012-06-20 Integrated set comprehension pointfree simproc.
2012-06-01 huffman 2012-06-01 remove duplicate lemma card_unit in favor of Finite_Set.card_UNIV_unit
2012-03-30 huffman 2012-03-30 rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'
2012-03-30 huffman 2012-03-30 move lemma card_UNIV_bool from Nat_Numeral.thy to Finite_Set.thy
2012-03-13 wenzelm 2012-03-13 tuned proofs -- eliminated pointless chaining of facts after 'interpret';
2012-01-06 haftmann 2012-01-06 incorporated various theorems from theory More_Set into corpus
2011-12-29 haftmann 2011-12-29 qualified Finite_Set.fold
2011-12-24 haftmann 2011-12-24 finite type class instance for `set`
2011-10-18 bulwahn 2011-10-18 tuned
2011-09-14 hoelzl 2011-09-14 renamed Complete_Lattices lemmas, removed legacy names
2011-09-13 noschinl 2011-09-13 tune proofs
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-09-06 haftmann 2011-09-06 merged
2011-09-05 haftmann 2011-09-05 tuned
2011-09-06 nipkow 2011-09-06 added new lemmas
2011-07-27 hoelzl 2011-07-27 finite vimage on arbitrary domains
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