src/HOL/Set.thy
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
2009-07-21 haftmann 2009-07-21 swapped bootstrap order of UNION/Union and INTER/Inter in theory Set
2009-07-20 haftmann 2009-07-20 less digestible
2009-07-20 haftmann 2009-07-20 refined outline structure
2009-07-20 haftmann 2009-07-20 merged
2009-07-20 haftmann 2009-07-20 closer relation of sets and complete lattices; corresponding consts, defs and syntax at similar places in theory text
2009-07-20 haftmann 2009-07-20 merged
2009-07-14 haftmann 2009-07-14 refinement of lattice classes
2009-07-15 wenzelm 2009-07-15 more antiquotations;
2009-07-11 haftmann 2009-07-11 added boolean_algebra type class; tuned lattice duals
2009-07-06 wenzelm 2009-07-06 structure Thm: less pervasive names;
2009-06-15 haftmann 2009-06-15 authentic syntax for Pow and image
2009-06-05 haftmann 2009-06-05 merged
2009-06-04 haftmann 2009-06-04 insert now qualified and with authentic syntax
2009-06-04 nipkow 2009-06-04 finite lemmas
2009-05-18 nipkow 2009-05-18 fine-tuned elimination of comprehensions involving x=t.
2009-05-16 nipkow 2009-05-16 "{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}" by the new simproc defColl_regroup. More precisely, the simproc pulls an equation x=t (or t=x) out of a nest of conjunctions to the front where the simp rule singleton_conj_conv(2) converts to "if".
2009-03-31 wenzelm 2009-03-31 tuned;
2009-03-19 haftmann 2009-03-19 tuned some theorem and attribute bindings
2009-03-14 haftmann 2009-03-14 reverted to old version of Set.thy -- strange effects have to be traced first
2009-03-07 haftmann 2009-03-07 restructured theory Set.thy
2009-03-05 haftmann 2009-03-05 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
2009-02-13 nipkow 2009-02-13 finiteness lemmas
2009-01-29 berghofe 2009-01-29 Added strong congruence rule for UN.
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-08-11 haftmann 2008-08-11 rudimentary code setup for set operations
2008-07-01 huffman 2008-07-01 remove simp attribute from range_composition
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