src/HOL/Set.thy
17 months ago wenzelm 2017-11-26 more symbols;
17 months ago haftmann 2017-11-11 dedicated definition for coprimality
18 months ago haftmann 2017-10-08 canonical introduction and destruction rules for pairwise
2016-09-29 hoelzl 2016-09-29 HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
2016-09-28 paulson 2016-09-28 new material connected with HOL Light measure theory, plus more rationalisation
2016-09-22 paulson 2016-09-22 More mainly topological results
2016-09-15 paulson 2016-09-15 simple new lemmas, mostly about sets
2016-08-02 wenzelm 2016-08-02 misc tuning and modernization;
2016-07-05 wenzelm 2016-07-05 misc tuning and modernization;
2016-07-05 wenzelm 2016-07-05 tuned;
2016-07-02 haftmann 2016-07-02 more theorems
2016-06-19 wenzelm 2016-06-19 misc tuning and modernization;
2016-06-14 paulson 2016-06-14 new results about topology
2016-05-27 wenzelm 2016-05-27 tuned proofs;
2016-05-23 paulson 2016-05-23 Lots of new material for multivariate analysis
2016-05-17 eberlm 2016-05-17 Moved material from AFP/Randomised_Social_Choice to distribution
2016-05-09 paulson 2016-05-09 renamings and refinements
2016-04-18 paulson 2016-04-18 new theorems about convex hulls, etc.; also, renamed some theorems
2016-04-04 paulson 2016-04-04 Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
2016-03-05 wenzelm 2016-03-05 old HOL syntax is for input only;
2016-02-23 nipkow 2016-02-23 more canonical names
2016-01-07 paulson 2016-01-07 revisions to limits and derivatives, plus new lemmas
2016-01-06 hoelzl 2016-01-06 add the proof of the central limit theorem
2015-12-28 wenzelm 2015-12-28 former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-10-26 paulson 2015-10-26 new lemmas about topology, etc., for Cauchy integral formula
2015-10-09 wenzelm 2015-10-09 discontinued specific HTML syntax;
2015-10-02 paulson 2015-10-02 New theorems about connected sets. And pairwise moved to Set.thy.
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-05-01 nipkow 2015-05-01 new simp rule
2015-04-14 Andreas Lochbihler 2015-04-14 add lemmas
2015-02-11 paulson 2015-02-11 Merge
2015-02-10 paulson 2015-02-10 Not a simprule, as it complicates proofs
2015-02-10 paulson 2015-02-10 New lemmas and a bit of tidying up.
2015-02-10 wenzelm 2015-02-10 misc tuning;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-13 hoelzl 2014-11-13 import general theorems from AFP/Markov_Models
2014-11-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-04-26 haftmann 2014-04-26 tuned
2014-03-13 haftmann 2014-03-13 tuned proofs
2014-03-09 haftmann 2014-03-09 tuned; elimination rule subset_imageE; typical composition collapsing rewrite order in lemma image_image_eq_image_comp; destruction rules ball_imageD, bex_imageD
2014-02-27 paulson 2014-02-27 A bit of tidying up
2014-01-25 wenzelm 2014-01-25 explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
2014-01-12 wenzelm 2014-01-12 tuned signature; clarified context;
2013-10-18 blanchet 2013-10-18 killed most "no_atp", to make Sledgehammer more complete
2013-09-02 nipkow 2013-09-02 added lemmas
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-12 wenzelm 2013-04-12 modifiers for classical wrappers operate on Proof.context instead of claset;
2013-03-12 nipkow 2013-03-12 extended set comprehension notation with {pttrn : A . P}
2013-03-05 nipkow 2013-03-05 more lemmas about intervals
2013-02-17 haftmann 2013-02-17 Sieve of Eratosthenes
2012-12-17 nipkow 2012-12-17 made element and subset relations non-associative (just like all orderings)
2012-10-09 kuncar 2012-10-09 rename Set.project to Set.filter - more appropriate name
2012-09-29 wenzelm 2012-09-29 more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
2012-04-06 haftmann 2012-04-06 tuned
2012-03-12 noschinl 2012-03-12 tuned simpset
2012-03-09 haftmann 2012-03-09 beautified