src/HOL/Finite_Set.thy
2016-10-01 wenzelm 2016-10-01 tuned;
2016-09-18 wenzelm 2016-09-18 tuned proofs;
2016-08-10 nipkow 2016-08-10 "split add" -> "split"
2016-08-05 wenzelm 2016-08-05 misc tuning and modernization;
2016-07-29 Andreas Lochbihler 2016-07-29 add lemmas contributed by Peter Gammie
2016-07-06 wenzelm 2016-07-06 misc tuning and modernization;
2016-07-02 haftmann 2016-07-02 more theorems
2016-05-17 eberlm 2016-05-17 Moved material from AFP/Randomised_Social_Choice to distribution
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-03-14 paulson 2016-03-14 Refactoring (moving theorems into better locations), plus a bit of new material
2016-03-01 haftmann 2016-03-01 tuned bootstrap order to provide type classes in a more sensible order
2016-02-23 nipkow 2016-02-23 more canonical names
2016-01-07 wenzelm 2016-01-07 more uniform treatment of package internals;
2015-12-19 haftmann 2015-12-19 abandoned attempt to unify sublocale and interpretation into global theories
2015-12-09 paulson 2015-12-09 sorted out eventually_mono
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-12-03 haftmann 2015-12-03 modernized
2015-12-01 paulson 2015-12-01 Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
2015-11-15 wenzelm 2015-11-15 option "inductive_defs" controls exposure of def and mono facts;
2015-11-09 wenzelm 2015-11-09 qualifier is mandatory by default;
2015-11-04 ballarin 2015-11-04 Keyword 'rewrites' identifies rewrite morphisms.
2015-10-26 paulson 2015-10-26 new lemmas about topology, etc., for Cauchy integral formula
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-07-20 paulson 2015-07-20 new material for multivariate analysis, etc.
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-06-27 wenzelm 2015-06-27 premises in 'show' are treated like 'assume';
2015-06-26 wenzelm 2015-06-26 tuned whitespace;
2015-05-26 paulson 2015-05-26 New material about paths, and some lemmas
2015-02-11 Andreas Lochbihler 2015-02-11 add lema about card and vimage
2015-02-11 Andreas Lochbihler 2015-02-11 add more general version of finite_vimageD
2015-02-10 paulson 2015-02-10 New lemmas and a bit of tidying up.
2015-01-10 nipkow 2015-01-10 added lemma
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
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