2002-05-07 ago use eq_thm_prop instead of slightly inadequate eq_thm;
1999-09-29 ago Sign.defaultS;
1999-07-10 ago handle THM exn;
1998-11-25 ago replaced prs by std_output / writeln;
1997-11-21 ago changed Pure/Sequence interface -- isatool fixseq;
1997-07-22 ago Removal of the tactical STATE
1996-11-28 ago Replaced map...~~ by
1996-02-16 ago Elimination of fully-functorial style.
1994-09-14 ago now uses Sign.const_type;
1994-01-18 ago Updated refs to old Sign functions
1993-09-16 ago changed addcongs to addeqcongs in simplifier.ML
1993-09-16 ago Initial revision