src/HOL/Finite_Set.thy
2014-09-06 haftmann 2014-09-06 added various facts
2014-07-21 Andreas Lochbihler 2014-07-21 add lemma
2014-06-30 hoelzl 2014-06-30 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
2014-05-20 hoelzl 2014-05-20 add various lemmas
2014-03-19 haftmann 2014-03-19 elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
2014-03-16 haftmann 2014-03-16 normalising simp rules for compound operators
2014-03-15 haftmann 2014-03-15 more complete set of lemmas wrt. image and composition
2014-01-21 traytel 2014-01-21 removed theory dependency of BNF_LFP on Datatype
2014-01-20 blanchet 2014-01-20 swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)
2014-01-16 blanchet 2014-01-16 dissolved 'Fun_More_FP' (a BNF dependency)
2013-12-28 haftmann 2013-12-28 prefix disambiguation
2013-12-26 haftmann 2013-12-26 prefer ephemeral interpretation over interpretation in proof contexts; prefer context begin ... end blocks for often-occuring assumptions; slightly more complete interpretations into abstract algebraic structures for gcd/lcm
2013-11-29 traytel 2013-11-29 set_comprehension_pointfree simproc causes to many surprises if enabled by default
2013-11-24 paulson 2013-11-24 polished some ancient proofs
2013-11-12 hoelzl 2013-11-12 add finite_select_induct; move generic lemmas from MV_Analysis/Linear_Algebra to the HOL image
2013-10-18 blanchet 2013-10-18 killed more "no_atp"s
2013-10-18 blanchet 2013-10-18 killed most "no_atp", to make Sledgehammer more complete
2013-09-24 nipkow 2013-09-24 added lemmas
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-04-04 haftmann 2013-04-04 convenient induction rule
2013-04-03 haftmann 2013-04-03 generalized lemma fold_image thanks to Peter Lammich
2013-03-26 haftmann 2013-03-26 more uniform style for interpretation and sublocale declarations
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