src/HOL/Set.thy
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
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
2010-02-04 hoelzl 2010-02-04 Changed 'bounded unique existential quantifiers' from a constant to syntax translation.
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2009-12-30 krauss 2009-12-30 killed a few warnings
2009-11-27 berghofe 2009-11-27 Removed eq_to_mono2, added not_mono.
2009-11-09 paulson 2009-11-09 New theory Probability/Borel.thy, and some associated lemmas
2009-10-21 paulson 2009-10-21 merged
2009-10-20 paulson 2009-10-20 Some new lemmas concerning sets
2009-10-21 haftmann 2009-10-21 merged
2009-10-21 haftmann 2009-10-21 dropped redundant gen_ prefix
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-20 paulson 2009-10-20 Removal of the unused atpset concept, the atp attribute and some related code.
2009-10-07 haftmann 2009-10-07 tuned proofs
2009-09-19 haftmann 2009-09-19 inter and union are mere abbreviations for inf and sup
2009-08-31 nipkow 2009-08-31 tuned the simp rules for Int involving insert and intervals.
2009-07-28 haftmann 2009-07-28 Set.UNIV and Set.empty are mere abbreviations for top and bot
2009-07-22 haftmann 2009-07-22 moved complete_lattice &c. into separate theory
2009-07-22 haftmann 2009-07-22 set intersection and union now named inter and union; closer connection between set and lattice operations; factored out complete lattice
2009-07-21 haftmann 2009-07-21 attempt for more concise setup of non-etacontracting binders
2009-07-21 haftmann 2009-07-21 Set.thy: prefer = over == where possible; tuned ML setup; dropped (moved) ML legacy
2009-07-21 haftmann 2009-07-21 swapped bootstrap order of UNION/Union and INTER/Inter in theory Set
2009-07-20 haftmann 2009-07-20 less digestible
2009-07-20 haftmann 2009-07-20 refined outline structure
2009-07-20 haftmann 2009-07-20 merged
2009-07-20 haftmann 2009-07-20 closer relation of sets and complete lattices; corresponding consts, defs and syntax at similar places in theory text
2009-07-20 haftmann 2009-07-20 merged
2009-07-14 haftmann 2009-07-14 refinement of lattice classes
2009-07-15 wenzelm 2009-07-15 more antiquotations;
2009-07-11 haftmann 2009-07-11 added boolean_algebra type class; tuned lattice duals
2009-07-06 wenzelm 2009-07-06 structure Thm: less pervasive names;
2009-06-15 haftmann 2009-06-15 authentic syntax for Pow and image
2009-06-05 haftmann 2009-06-05 merged
2009-06-04 haftmann 2009-06-04 insert now qualified and with authentic syntax
2009-06-04 nipkow 2009-06-04 finite lemmas
2009-05-18 nipkow 2009-05-18 fine-tuned elimination of comprehensions involving x=t.
2009-05-16 nipkow 2009-05-16 "{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}" by the new simproc defColl_regroup. More precisely, the simproc pulls an equation x=t (or t=x) out of a nest of conjunctions to the front where the simp rule singleton_conj_conv(2) converts to "if".
2009-03-31 wenzelm 2009-03-31 tuned;
2009-03-19 haftmann 2009-03-19 tuned some theorem and attribute bindings
2009-03-14 haftmann 2009-03-14 reverted to old version of Set.thy -- strange effects have to be traced first
2009-03-07 haftmann 2009-03-07 restructured theory Set.thy
2009-03-05 haftmann 2009-03-05 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
2009-02-13 nipkow 2009-02-13 finiteness lemmas