src/FOL/simpdata.ML
2005-12-31 ago removed obsolete Provers/make_elim.ML;
2005-12-01 ago unfold_tac: static evaluation of simpset;
2005-10-18 ago Simplifier.theory_context;
2005-10-17 ago change_claset/simpset;
2005-09-12 ago introduced new-style AList operations
2005-08-02 ago simprocs: Simplifier.inherit_bounds;
2005-05-22 ago Simplifier already setup in Pure;
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2002-08-06 ago sane interface for simprocs;
2002-05-15 ago better simplification of trivial existential equalities
2002-01-21 ago new simprules and classical rules
2002-01-15 ago new theorem
2002-01-12 ago renamed forall_elim_vars_safe to gen_all;
2002-01-11 ago replace gen_all by forall_elim_vars_safe;
2001-12-17 ago mods due to changed 1-point simprocs (quantifier1).
2001-11-03 ago proper use of bind_thm(s);
2001-10-14 ago moved rulify to ObjectLogic;
2001-10-14 ago eliminated atomize rules;
2001-05-31 ago streamlined addIffs/delIffs, added warnings
2001-03-29 ago generalization of 1 point rules for ALL
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,