src/HOL/Set.ML
1997-11-20 paulson 1997-11-20 Renamed "overload" to "overloaded" for sml/nj compatibility
1997-11-16 nipkow 1997-11-16 Removed "(ALL x:f``A. P x) = (ALL x:A. P(f x))", "(EX x:f``A. P x) = (EX x:A. P(f x))", again, because they were already there and added "(UN x:f``A. B x) = (UN a:A. B(f a))" "(INT x:f``A. B x) = (INT a:A. B(f a))" instead.
1997-11-15 nipkow 1997-11-15 Added > "(? x : f `` A. P x) = (? a:A. P(f a))" > "(! x : f `` A. P x) = (! a:A. P(f a))"
1997-11-05 paulson 1997-11-05 UNIV now a constant; UNION1, INTER1 now translations and no longer have separate rules for themselves
1997-11-04 oheimb 1997-11-04 removed redundant ball_empty and bex_empty (see equalities.ML)
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-11-01 paulson 1997-11-01 New Blast_tac (and minor tidying...)
1997-10-21 paulson 1997-10-21 New rewrite rules image_iff
1997-10-17 nipkow 1997-10-17 setloop split_tac -> addsplits
1997-10-17 paulson 1997-10-17 New rewrite rules for simplifying conditionals
1997-10-17 nipkow 1997-10-17 Added image_eqI to simpset.
1997-10-16 nipkow 1997-10-16 Modified comment.
1997-10-16 nipkow 1997-10-16 Various new lemmas. Improved conversion of equations to rewrite rules: (s=t becomes (s=t)==True if s=t loops).
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-09-26 paulson 1997-09-26 Minor tidying to use Clarify_tac, etc.
1997-08-01 nipkow 1997-08-01 Added {x.x=a} = a to !simpset.
1997-07-01 paulson 1997-07-01 Now Collect_mem_eq is a default simprule (how could it have ever been omitted?
1997-06-06 paulson 1997-06-06 New miniscoping rules ball_triv and bex_triv
1997-05-16 nipkow 1997-05-16 Distributed Psubset stuff to basic set theory files, incl Finite. Added stuff by bu.
1997-04-11 paulson 1997-04-11 Yet more fast_tac->blast_tac, and other tidying
1997-04-04 nipkow 1997-04-04 moved inj and surj from Set to Fun and Inv -> inv.
1997-04-04 paulson 1997-04-04 Calls Blast_tac
1997-04-03 paulson 1997-04-03 Declares overloading for set-theoretic constants
1997-04-02 paulson 1997-04-02 Re-ordering of rules to assist blast_tac Powerset rules must not be the most recent
1997-03-05 paulson 1997-03-05 New version of InterE, like its ZF counterpart
1997-02-12 nipkow 1997-02-12 New class "order" and accompanying changes. In particular reflexivity of <= is now one rewrite rule.
1997-01-09 paulson 1997-01-09 Tidying of proofs. New theorems are enterred immediately into the relevant clasets or simpsets.
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-09-25 paulson 1996-09-25 Rationalized the rewriting of membership for {} and insert by deleting the redundant theorems in_empty and in_insert
1996-09-12 paulson 1996-09-12 Tidied many proofs, using AddIffs to let equivalences take the place of separate Intr and Elim rules. Also deleted most named clasets.
1996-08-22 paulson 1996-08-22 Proved mem_if
1996-08-19 paulson 1996-08-19 Added impOfSubs
1996-07-26 paulson 1996-07-26 Proved bex_False
1996-06-28 paulson 1996-06-28 Added contra_subsetD and rev_contra_subsetD
1996-06-18 paulson 1996-06-18 New rewrites for vacuous quantification
1996-05-31 oheimb 1996-05-31 moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML, as there have been unnecessary proofs of anonymous thms, which could not be removed (by name) from the !simpset where necessary. All these thms except singleton_iff were already proved in Set.ML. therefore in Set.ML: New version of singletonE, proof of new thm singleton_iff
1996-05-23 berghofe 1996-05-23 equalityI is now added to default claset
1996-05-23 berghofe 1996-05-23 Replaced fast_tac by Fast_tac (which uses default claset) New rules are now also added to default claset.
1996-04-04 paulson 1996-04-04 Added more _iff rewrites for Compl, Un, Int
1996-03-27 paulson 1996-03-27 Library changes for mutilated checkerboard
1996-03-06 paulson 1996-03-06 Ran expandshort
1996-03-06 nipkow 1996-03-06 Added 'section' commands
1996-03-04 nipkow 1996-03-04 Added a constant UNIV == {x.True} Added many new rewrite rules for sets. Moved LEAST into Nat. Added cardinality to Finite.
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application