src/HOL/Set.thy
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
2012-02-16 bulwahn 2012-02-16 removing unnecessary premise from diff_single_insert
2012-02-14 wenzelm 2012-02-14 eliminated obsolete aliases;
2012-01-07 haftmann 2012-01-07 massaging of code setup for sets
2012-01-06 haftmann 2012-01-06 incorporated various theorems from theory More_Set into corpus
2012-01-06 wenzelm 2012-01-06 tuned -- more direct @{type_name set} (NB: binder_tr' retains the original non-syntax type for the bound/free variable);
2012-01-01 haftmann 2012-01-01 interaction of set operations for execution and membership predicate
2012-01-01 haftmann 2012-01-01 cleanup of code declarations
2011-12-29 haftmann 2011-12-29 fundamental theorems on Set.bind
2011-12-29 haftmann 2011-12-29 semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat
2011-12-26 haftmann 2011-12-26 moved various set operations to theory Set (resp. Product_Type)
2011-12-24 haftmann 2011-12-24 `set` is now a proper type constructor; added operation for set monad
2011-12-17 wenzelm 2011-12-17 tuned signature;
2011-11-27 wenzelm 2011-11-27 just one data slot per module; tuned;
2011-11-24 wenzelm 2011-11-24 modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-10-16 haftmann 2011-10-16 hide not_member as also member
2011-10-09 huffman 2011-10-09 Set.thy: remove redundant [simp] declarations
2011-09-06 nipkow 2011-09-06 added new lemmas
2011-08-25 krauss 2011-08-25 lemma Compl_insert: "- insert x A = (-A) - {x}"
2011-08-17 wenzelm 2011-08-17 modernized signature of Term.absfree/absdummy; eliminated obsolete Term.list_abs_free;
2011-07-24 haftmann 2011-07-24 more coherent structure in and across theories
2011-07-18 haftmann 2011-07-18 moved lemmas to appropriate theory
2011-07-17 haftmann 2011-07-17 moving UNIV = ... equations to their proper theories
2011-07-14 haftmann 2011-07-14 tuned lemma positions and proofs
2011-04-22 wenzelm 2011-04-22 misc tuning and simplification;
2011-04-22 wenzelm 2011-04-22 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61); tuned signature;
2011-04-22 wenzelm 2011-04-22 modernized Quantifier1 simproc setup;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Mixfix; eliminated slightly odd no_syn convenience;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-03-30 bulwahn 2011-03-30 renewing specifications in HOL: replacing types by type_synonym