src/HOL/subset.ML
1998-08-13 paulson 1998-08-13 even more tidying of Goal commands
1997-11-05 paulson 1997-11-05 UNIV now a constant; UNION1, INTER1 now translations and no longer have separate rules for themselves
1997-04-04 paulson 1997-04-04 Calls Blast_tac. Tidied some proofs
1997-01-17 paulson 1997-01-17 Deleted the redundant theorem subset_empty_iff (subset_empty exists already)
1996-05-23 berghofe 1996-05-23 Removed equalityI from some proofs (because it is now included in the 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-03-29 paulson 1996-03-29 new lemma for mutilated chess board
1996-03-06 paulson 1996-03-06 Ran expandshort
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