1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-08-06 berghofe 1997-08-06 Moved some functions which used to be part of thy_data.ML
1997-04-21 paulson 1997-04-21 New elimination rule for "unique existence"
1997-04-03 paulson 1997-04-03 Declares overloading for if-and-only-if
1997-04-02 paulson 1997-04-02 Installation of 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.