src/Provers/simp.ML
2002-05-07 wenzelm 2002-05-07 use eq_thm_prop instead of slightly inadequate eq_thm;
1999-09-29 wenzelm 1999-09-29 Sign.defaultS;
1999-07-10 wenzelm 1999-07-10 handle THM exn;
1998-11-25 wenzelm 1998-11-25 replaced prs by std_output / writeln;
1997-11-21 wenzelm 1997-11-21 changed Pure/Sequence interface -- isatool fixseq;
1997-07-22 paulson 1997-07-22 Removal of the tactical STATE
1996-11-28 paulson 1996-11-28 Replaced map...~~ by ListPair.map
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1994-09-14 wenzelm 1994-09-14 now uses Sign.const_type;
1994-01-18 lcp 1994-01-18 Updated refs to old Sign functions
1993-09-16 nipkow 1993-09-16 changed addcongs to addeqcongs in simplifier.ML
1993-09-16 clasohm 1993-09-16 Initial revision