src/HOL/Set.thy
2008-06-10 haftmann 2008-06-10 removed some dubious code lemmas
2008-05-07 berghofe 2008-05-07 - Now uses Orderings as parent theory - "'a set" is now just a type abbreviation for "'a => bool" - The instantiation "set :: (type) ord" and the definition of (p)subset is no longer needed, since it is subsumed by the order on functions and booleans. The derived theorems (p)subset_eq can be used as a replacement. - mem_Collect_eq and Collect_mem_eq can now be derived from the definitions of mem and Collect. - Replaced the instantiation "set :: (type) minus" by the two instantiations "fun :: (type, minus) minus" and "bool :: minus". The theorem set_diff_eq can be used as a replacement for the definition set_diff_def - Replaced the instantiation "set :: (type) uminus" by the two instantiations "fun :: (type, uminus) uminus" and "bool :: uminus". The theorem Compl_eq can be used as a replacement for the definition Compl_def. - Variable P in rule split_if must be instantiated manually in proof of split_if_mem2 due to problems with HO unification - Moved definition of dense linear orders and proofs about LEAST from Orderings to Set - Deleted code setup for sets
2008-04-22 haftmann 2008-04-22 constant HOL.eq now qualified
2008-04-02 haftmann 2008-04-02 explicit class "eq" for operational equality
2008-03-29 wenzelm 2008-03-29 replaced 'ML_setup' by 'ML';
2008-03-19 wenzelm 2008-03-19 eliminated change_claset/simpset;
2008-02-26 haftmann 2008-02-26 moved some set lemmas from Set.thy here
2008-01-25 haftmann 2008-01-25 improved code theorem setup
2008-01-02 haftmann 2008-01-02 splitted class uminus from class minus
2007-11-30 haftmann 2007-11-30 adjustions to due to instance target
2007-11-29 haftmann 2007-11-29 instance command as rudimentary class target
2007-11-23 haftmann 2007-11-23 interpretation of typedecls: instantiation to class type
2007-11-09 krauss 2007-11-09 avoid name clashes when generating code for union, inter
2007-11-05 nipkow 2007-11-05 added lemmas
2007-09-26 haftmann 2007-09-26 convenient obtain rule for sets
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;