src/HOL/Set.thy
2007-09-20 haftmann 2007-09-20 clarified code lemmas
2007-08-24 haftmann 2007-08-24 made sets executable
2007-08-19 nipkow 2007-08-19 Made UN_Un simp
2007-08-17 haftmann 2007-08-17 dropped junk
2007-08-15 paulson 2007-08-15 ATP blacklisting is now in theory data, attribute noatp
2007-08-15 haftmann 2007-08-15 updated code generator setup
2007-07-20 haftmann 2007-07-20 simplified HOL bootstrap
2007-07-19 haftmann 2007-07-19 code lemma for contents
2007-05-06 haftmann 2007-05-06 changed code generator invocation syntax
2007-04-20 haftmann 2007-04-20 Isar definitions are now added explicitly to code theorem table
2007-03-20 haftmann 2007-03-20 fixed typo
2007-03-16 haftmann 2007-03-16 added instance of sets as distributive lattices
2007-03-12 wenzelm 2007-03-12 syntax: proper body priorty for derived binders;
2007-02-28 wenzelm 2007-02-28 tuned ML setup;
2007-01-24 paulson 2007-01-24 some new lemmas
2007-01-20 wenzelm 2007-01-20 tuned ML setup;
2006-12-13 haftmann 2006-12-13 dropped FIXME comment
2006-12-13 haftmann 2006-12-13 fixed syntax for bounded quantification
2006-12-06 wenzelm 2006-12-06 removed legacy ML bindings;
2006-11-27 haftmann 2006-11-27 restructured some proofs
2006-11-26 wenzelm 2006-11-26 updated (binder) syntax/notation;
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-15 haftmann 2006-11-15 moved transitivity rules to Orderings.thy
2006-11-13 haftmann 2006-11-13 dropped LOrder dependency
2006-11-12 nipkow 2006-11-12 image_constant_conv no longer [simp]
2006-11-12 nipkow 2006-11-12 started reorgnization of lattice theories
2006-11-07 wenzelm 2006-11-07 renamed 'const_syntax' to 'notation';
2006-08-14 haftmann 2006-08-14 simplified code generator setup
2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs)
2006-06-13 paulson 2006-06-13 new results
2006-05-16 wenzelm 2006-05-16 tuned concrete syntax -- abbreviation/const_syntax;
2006-05-13 wenzelm 2006-05-13 reactivated translations for less/less_eq;
2006-04-08 wenzelm 2006-04-08 refined 'abbreviation';
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