src/HOL/Set.thy
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
2010-12-10 haftmann 2010-12-10 moved most fundamental lemmas upwards
2010-12-08 haftmann 2010-12-08 bot comes before top, inf before sup etc.
2010-12-08 haftmann 2010-12-08 primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`; tuned
2010-12-02 hoelzl 2010-12-02 Move SUP_commute, SUP_less_iff to HOL image; Cleanup generic complete_lattice lemmas in Positive_Infinite_Real; Cleanup lemma positive_integral_alt;
2010-11-23 hoelzl 2010-11-23 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
2010-10-01 haftmann 2010-10-01 constant `contents` renamed to `the_elem`
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-08 nipkow 2010-09-08 put expand_(fun/set)_eq back in as synonyms, for compatibility
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-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-26 haftmann 2010-08-26 formerly unnamed infix impliciation now named HOL.implies
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-08-23 blanchet 2010-08-23 "no_atp" fact that leads to unsound proofs
2010-08-23 blanchet 2010-08-23 "no_atp" a few facts that often lead to unsound proofs
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-07-01 haftmann 2010-07-01 qualified constants Set.member and Set.Collect
2010-06-08 haftmann 2010-06-08 qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
2010-03-28 huffman 2010-03-28 use lattice theorems to prove set theorems
2010-03-18 blanchet 2010-03-18 now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-03-04 hoelzl 2010-03-04 Added vimage_inter_cong