src/HOL/Set.thy
 2009-02-13 nipkow 2009-02-13 finiteness lemmas file | diff | annotate 2009-01-29 berghofe 2009-01-29 Added strong congruence rule for UN. file | diff | annotate 2008-10-10 haftmann 2008-10-10 `code func` now just `code` file | diff | annotate 2008-08-11 haftmann 2008-08-11 rudimentary code setup for set operations file | diff | annotate 2008-07-01 huffman 2008-07-01 remove simp attribute from range_composition file | diff | annotate 2008-06-10 haftmann 2008-06-10 removed some dubious code lemmas file | diff | annotate 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 file | diff | annotate 2008-04-22 haftmann 2008-04-22 constant HOL.eq now qualified file | diff | annotate 2008-04-02 haftmann 2008-04-02 explicit class "eq" for operational equality file | diff | annotate 2008-03-29 wenzelm 2008-03-29 replaced 'ML_setup' by 'ML'; file | diff | annotate 2008-03-19 wenzelm 2008-03-19 eliminated change_claset/simpset; file | diff | annotate 2008-02-26 haftmann 2008-02-26 moved some set lemmas from Set.thy here file | diff | annotate 2008-01-25 haftmann 2008-01-25 improved code theorem setup file | diff | annotate 2008-01-02 haftmann 2008-01-02 splitted class uminus from class minus file | diff | annotate 2007-11-30 haftmann 2007-11-30 adjustions to due to instance target file | diff | annotate 2007-11-29 haftmann 2007-11-29 instance command as rudimentary class target file | diff | annotate 2007-11-23 haftmann 2007-11-23 interpretation of typedecls: instantiation to class type file | diff | annotate 2007-11-09 krauss 2007-11-09 avoid name clashes when generating code for union, inter file | diff | annotate 2007-11-05 nipkow 2007-11-05 added lemmas file | diff | annotate 2007-09-26 haftmann 2007-09-26 convenient obtain rule for sets file | diff | annotate 2007-09-20 haftmann 2007-09-20 clarified code lemmas file | diff | annotate 2007-08-24 haftmann 2007-08-24 made sets executable file | diff | annotate 2007-08-19 nipkow 2007-08-19 Made UN_Un simp file | diff | annotate 2007-08-17 haftmann 2007-08-17 dropped junk file | diff | annotate 2007-08-15 paulson 2007-08-15 ATP blacklisting is now in theory data, attribute noatp file | diff | annotate 2007-08-15 haftmann 2007-08-15 updated code generator setup file | diff | annotate 2007-07-20 haftmann 2007-07-20 simplified HOL bootstrap file | diff | annotate 2007-07-19 haftmann 2007-07-19 code lemma for contents file | diff | annotate 2007-05-06 haftmann 2007-05-06 changed code generator invocation syntax file | diff | annotate 2007-04-20 haftmann 2007-04-20 Isar definitions are now added explicitly to code theorem table file | diff | annotate 2007-03-20 haftmann 2007-03-20 fixed typo file | diff | annotate 2007-03-16 haftmann 2007-03-16 added instance of sets as distributive lattices file | diff | annotate 2007-03-12 wenzelm 2007-03-12 syntax: proper body priorty for derived binders; file | diff | annotate 2007-02-28 wenzelm 2007-02-28 tuned ML setup; file | diff | annotate 2007-01-24 paulson 2007-01-24 some new lemmas file | diff | annotate 2007-01-20 wenzelm 2007-01-20 tuned ML setup; file | diff | annotate 2006-12-13 haftmann 2006-12-13 dropped FIXME comment file | diff | annotate 2006-12-13 haftmann 2006-12-13 fixed syntax for bounded quantification file | diff | annotate 2006-12-06 wenzelm 2006-12-06 removed legacy ML bindings; file | diff | annotate 2006-11-27 haftmann 2006-11-27 restructured some proofs file | diff | annotate 2006-11-26 wenzelm 2006-11-26 updated (binder) syntax/notation; file | diff | annotate 2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation; file | diff | annotate 2006-11-15 haftmann 2006-11-15 moved transitivity rules to Orderings.thy file | diff | annotate 2006-11-13 haftmann 2006-11-13 dropped LOrder dependency file | diff | annotate 2006-11-12 nipkow 2006-11-12 image_constant_conv no longer [simp] file | diff | annotate 2006-11-12 nipkow 2006-11-12 started reorgnization of lattice theories file | diff | annotate 2006-11-07 wenzelm 2006-11-07 renamed 'const_syntax' to 'notation'; file | diff | annotate 2006-08-14 haftmann 2006-08-14 simplified code generator setup file | diff | annotate 2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs) file | diff | annotate 2006-06-13 paulson 2006-06-13 new results file | diff | annotate 2006-05-16 wenzelm 2006-05-16 tuned concrete syntax -- abbreviation/const_syntax; file | diff | annotate 2006-05-13 wenzelm 2006-05-13 reactivated translations for less/less_eq; file | diff | annotate 2006-04-08 wenzelm 2006-04-08 refined 'abbreviation'; file | diff | annotate 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. file | diff | annotate 2006-03-20 paulson 2006-03-20 subsetI is often necessary file | diff | annotate 2006-03-17 haftmann 2006-03-17 renamed op < <= to Orderings.less(_eq) file | diff | annotate 2006-03-10 haftmann 2006-03-10 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc. file | diff | annotate 2006-03-02 paulson 2006-03-02 subset_refl now included using the atp attribute file | diff | annotate 2006-01-30 haftmann 2006-01-30 adaptions to codegen_package file | diff | annotate 2006-01-29 wenzelm 2006-01-29 declare 'defn' rules; file | diff | annotate