1997-04-04 paulson 1997-04-04 Calls Blast_tac
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-06-03 berghofe 1996-06-03 best_tac, deepen_tac and safe_tac now also use default claset.
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-04-04 paulson 1996-04-04 Using new "Times" infix
1996-03-11 paulson 1996-03-11 New, one-line proof of inj_Atom
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-02-09 nipkow 1996-02-09 Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-10-04 clasohm 1995-10-04 added local simpsets; removed IOA from 'make test'
1995-03-28 clasohm 1995-03-28 renamed theorem "apfst" to "apfst_conv" to avoid conflict with function apfst from Pure/library.ML
1995-03-24 clasohm 1995-03-24 changed syntax of tuples from <..., ...> to (..., ...)
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application