src/HOL/Set.ML
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