src/HOL/Set.thy
2006-03-23 nipkow 2006-03-23 Converted translations to abbbreviations. Removed a few odd functions from Map and AssocList. Moved chg_map from Map to Bali/Basis.
2006-03-20 paulson 2006-03-20 subsetI is often necessary
2006-03-17 haftmann 2006-03-17 renamed op < <= to Orderings.less(_eq)
2006-03-10 haftmann 2006-03-10 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
2006-03-02 paulson 2006-03-02 subset_refl now included using the atp attribute
2006-01-30 haftmann 2006-01-30 adaptions to codegen_package
2006-01-29 wenzelm 2006-01-29 declare 'defn' rules;
2006-01-13 nipkow 2006-01-13 *** empty log message ***
2005-12-21 paulson 2005-12-21 removed or modified some instances of [iff]
2005-12-16 nipkow 2005-12-16 new lemmas
2005-12-15 wenzelm 2005-12-15 removed obsolete/unused setup_induction;
2005-12-01 wenzelm 2005-12-01 simprocs: static evaluation of simpset;
2005-12-01 paulson 2005-12-01 restoring the old status of subset_refl
2005-11-10 paulson 2005-11-10 duplicate axioms in ATP linkup, and general fixes
2005-10-17 wenzelm 2005-10-17 change_claset/simpset; Simplifier.inherit_context instead of Simplifier.inherit_bounds;
2005-10-07 wenzelm 2005-10-07 Term.absdummy;
2005-09-29 paulson 2005-09-29 a name for empty_not_insert
2005-09-29 wenzelm 2005-09-29 more finalconsts;
2005-09-22 nipkow 2005-09-22 renamed rules to iprover
2005-09-20 wenzelm 2005-09-20 tuned theory dependencies;
2005-08-16 paulson 2005-08-16 more simprules now have names
2005-08-16 paulson 2005-08-16 classical rules must have names for ATP integration
2005-08-02 wenzelm 2005-08-02 simprocs: Simplifier.inherit_bounds;
2005-07-12 paulson 2005-07-12 tweaked
2005-07-01 berghofe 2005-07-01 Added strong_ball_cong and strong_bex_cong (these are now the standard congruence rules for Ball and Bex).
2005-05-11 nipkow 2005-05-11 Added thms by Brian Huffmann
2005-03-01 nipkow 2005-03-01 integrated Jeremy's FiniteLib
2005-02-18 nipkow 2005-02-18 tuning
2005-02-10 nipkow 2005-02-10 Moved oderings from HOL into the new Orderings.thy
2004-09-27 ballarin 2004-09-27 Modified locales: improved implementation of "includes".
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-08-06 nipkow 2004-08-06 undid UN/INT syntax
2004-08-03 paulson 2004-08-03 new simprules Int_subset_iff and Un_subset_iff
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-05-29 wenzelm 2004-05-29 \<^bsub>/\<^esub> syntax: unbreakable block;
2004-05-28 paulson 2004-05-28 new theorem Collect_imp_eq
2004-05-26 nipkow 2004-05-26 Corrected printer bug for bounded quantifiers Q x<=y. P
2004-05-17 mehta 2004-05-17 lemma disjoint_int_union removed - too special
2004-05-13 mehta 2004-05-13 New simp rules added: insert_disjoint disjoint_insert disjoint_int_union
2004-05-01 wenzelm 2004-05-01 improved subscript syntax;
2004-04-14 kleing 2004-04-14 use more symbols in HTML output
2004-04-13 ballarin 2004-04-13 Various changes to HOL-Algebra; Locale instantiation.
2004-03-24 paulson 2004-03-24 streamlined treatment of quotients for the integers
2004-02-19 ballarin 2004-02-19 Efficient, graph-based reasoner for linear and partial orders. + Setup as solver in the HOL simplifier.
2004-02-11 nipkow 2004-02-11 Modified UN and INT xsymbol syntax: made index subscript
2004-01-01 paulson 2004-01-01 conversion of Real/PReal to Isar script; type "complex" is now in class "field"
2003-12-19 nipkow 2003-12-19 *** empty log message ***
2003-09-26 paulson 2003-09-26 misc tidying
2003-07-11 oheimb 2003-07-11 added rev_ballE
2003-03-17 paulson 2003-03-17 moved one proof, added another
2003-03-14 paulson 2003-03-14 new UN/INT simprules
2003-03-11 nipkow 2003-03-11 *** empty log message ***
2003-02-26 paulson 2003-02-26 new lemma
2003-02-25 nipkow 2003-02-25 Undid eta change for UN/INT.
2003-02-16 paulson 2003-02-16 new theorem Compl_partition2
2002-12-22 nipkow 2002-12-22 removed some problems with print translations
2002-12-22 nipkow 2002-12-22 added print translations tha avoid eta contraction for important binders.
2002-10-18 nipkow 2002-10-18 Added a few thms about UN/INT/{}/UNIV
2002-10-03 paulson 2002-10-03 added the new elim rule psubsetE