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
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