2000-11-10 ago FOL_basic_ss: simprocs moved to FOL_ss;
2000-09-07 ago rulify setup;
2000-09-05 ago iff declarations moved to clasimp.ML;
2000-08-29 ago cong setup now part of Simplifier;
2000-07-13 ago AddIffs now available for FOL, ZF
2000-03-31 ago added cong atts;
2000-03-15 ago clasimp: include Splitter;
1999-09-21 ago Mod because of new solver interface.
1999-08-25 ago proper bootstrap of IFOL/FOL theories and packages;
1999-03-17 ago Theory.sign_of;
1999-01-13 ago congruence rules finally use == instead of = and <->
1998-09-24 ago simplified CLASIMP_DATA
1998-09-18 ago Pruning of parameters and True assumptions
1998-08-12 ago minor adaption for SML/NJ
1998-08-12 ago the splitter is now defined as a functor
1998-07-30 ago made SML/NJ happy;
1998-07-30 ago functorized Clasimp module;
1998-07-02 ago HACKED declaration of addsplits
1998-05-14 ago extended addsplits and delsplits to handle also split rules for assumptions
1998-04-04 ago no open Simplifier;
1998-02-28 ago Splitters via named loopers.
1998-02-25 ago factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
1998-02-25 ago changed wrapper mechanism of classical reasoner
1997-12-24 ago New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-12-03 ago Instantiated the one-point-rule quantifier simpprocs for FOL
1997-11-28 ago addsplits now in FOL, ZF too
1997-11-12 ago renamed split_prem_tac to split_asm_tac
1997-11-07 ago added split_prem_tac
1997-11-07 ago changed libraray function find to find_index_eq, currying it
1997-11-03 ago adapted to new implicit simpset;
1997-10-17 ago New simprules imp_disj1,2 and some comments
1997-10-10 ago fixed dots;
1997-08-06 ago Moved functions from file "thy_data.ML".
1997-07-23 ago standard congs;
1997-07-22 ago Removal of the tactical STATE
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.