1997-05-15 ago renamed addss to addSss, unsafe_addss to addss, extended auto_tac
1997-03-18 ago Added P&P&Q <-> P&Q and P|P|Q <-> P|Q
1997-03-05 ago Eta-expanded declarations of addSIs2, etc., to avoid polymorphism errors
1997-02-15 ago added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
1997-02-10 ago Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
1997-01-03 ago Implicit simpsets and clasets for FOL and ZF
1996-10-09 ago Added the de Morgan laws (incl quantifier versions) to basic simpset
1996-10-08 ago Addition of one-point quantifier rewrite rules
1996-09-09 ago Removal of (EX x. P) <-> P and (ALL x. P) <-> P
1996-09-05 ago Introduction of miniscoping for FOL
1996-08-19 ago Added a lot of basic laws, from HOL/simpdata
1996-05-06 ago Added split_inside_tac.
1996-01-29 ago expanded tabs
1995-05-03 ago Imported meta_eq_to_obj_eq from HOL for use with 'split'.
1995-03-30 ago Defined addss to perform simplification in a claset.
1995-03-08 ago Enforced partial evaluation of mk_case_split_tac.
1994-12-14 ago conj_commute,disj_commute: new
1994-11-30 ago added qed_goal for meta_iffD
1994-11-25 ago added blank line
1994-06-17 ago atomize: borrowed HOL version, which checks for both Trueprop
1994-05-24 ago Modified mk_meta_eq to leave meta-equlities on unchanged.
1994-05-13 ago FOL/simpdata: added etac FalseE in setsolver call. Toby: "now that the
1994-03-17 ago FOL/simpdata: tidied
1994-01-05 ago updated solver of FOL_ss. see change of HOL/simpdata.ML
1993-10-12 ago Added gen_all to simpdata.ML.
1993-09-16 ago defined local addcongs
1993-09-16 ago Initial revision