src/FOL/simpdata.ML
2005-10-18 wenzelm 2005-10-18 Simplifier.theory_context;
2005-10-17 wenzelm 2005-10-17 change_claset/simpset; Simplifier.inherit_context instead of Simplifier.inherit_bounds;
2005-09-12 haftmann 2005-09-12 introduced new-style AList operations
2005-08-02 wenzelm 2005-08-02 simprocs: Simplifier.inherit_bounds;
2005-05-22 wenzelm 2005-05-22 Simplifier already setup in Pure;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2002-08-06 wenzelm 2002-08-06 sane interface for simprocs;
2002-05-15 paulson 2002-05-15 better simplification of trivial existential equalities
2002-01-21 paulson 2002-01-21 new simprules and classical rules
2002-01-15 paulson 2002-01-15 new theorem
2002-01-12 wenzelm 2002-01-12 renamed forall_elim_vars_safe to gen_all;
2002-01-11 wenzelm 2002-01-11 replace gen_all by forall_elim_vars_safe;
2001-12-17 nipkow 2001-12-17 mods due to changed 1-point simprocs (quantifier1).
2001-11-03 wenzelm 2001-11-03 proper use of bind_thm(s);
2001-10-14 wenzelm 2001-10-14 moved rulify to ObjectLogic;
2001-10-14 wenzelm 2001-10-14 eliminated atomize rules;
2001-05-31 oheimb 2001-05-31 streamlined addIffs/delIffs, added warnings
2001-03-29 nipkow 2001-03-29 generalization of 1 point rules for ALL
2000-11-10 wenzelm 2000-11-10 FOL_basic_ss: simprocs moved to FOL_ss;
2000-09-07 wenzelm 2000-09-07 rulify setup;
2000-09-05 wenzelm 2000-09-05 iff declarations moved to clasimp.ML;
2000-08-29 wenzelm 2000-08-29 cong setup now part of Simplifier;
2000-07-13 paulson 2000-07-13 AddIffs now available for FOL, ZF
2000-03-31 wenzelm 2000-03-31 added cong atts;
2000-03-15 wenzelm 2000-03-15 clasimp: include Splitter;
1999-09-21 nipkow 1999-09-21 Mod because of new solver interface.
1999-08-25 wenzelm 1999-08-25 proper bootstrap of IFOL/FOL theories and packages;
1999-03-17 wenzelm 1999-03-17 Theory.sign_of;
1999-01-13 paulson 1999-01-13 congruence rules finally use == instead of = and <->
1998-09-24 oheimb 1998-09-24 simplified CLASIMP_DATA renamed mk_meta_eq to mk_eq introduced new mk_meta_eq, simplified addcongs and delcongs, introducing mk_meta_cong
1998-09-18 paulson 1998-09-18 Pruning of parameters and True assumptions
1998-08-12 oheimb 1998-08-12 minor adaption for SML/NJ
1998-08-12 oheimb 1998-08-12 the splitter is now defined as a functor moved addsplits, delsplits, Addsplits, Delsplits to Provers/splitter.ML moved split_thm_info to Provers/splitter.ML definined atomize via general mk_atomize removed superfluous rot_eq_tac from simplifier.ML HOL/simpdata.ML: renamed mk_meta_eq to meta_eq, re-renamed mk_meta_eq_simp to mk_meta_eq added Eps_eq to simpset
1998-07-30 wenzelm 1998-07-30 made SML/NJ happy;
1998-07-30 wenzelm 1998-07-30 functorized Clasimp module;
1998-07-02 paulson 1998-07-02 HACKED declaration of addsplits
1998-05-14 oheimb 1998-05-14 extended addsplits and delsplits to handle also split rules for assumptions extended const_of_split_thm, renamed it to split_thm_info
1998-04-04 wenzelm 1998-04-04 no open Simplifier;
1998-02-28 nipkow 1998-02-28 Splitters via named loopers.
1998-02-25 oheimb 1998-02-25 factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning combination of classical reasoner and simplifier auto_tac into Provers/clasimp.ML explicitly introducing combined type clasimpset
1998-02-25 oheimb 1998-02-25 changed wrapper mechanism of classical reasoner
1997-12-24 paulson 1997-12-24 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-12-03 paulson 1997-12-03 Instantiated the one-point-rule quantifier simpprocs for FOL New file fologic.ML holds abstract syntax operations Also, miniscoping provided for intuitionistic logic
1997-11-28 paulson 1997-11-28 addsplits now in FOL, ZF too
1997-11-12 oheimb 1997-11-12 renamed split_prem_tac to split_asm_tac
1997-11-07 oheimb 1997-11-07 added split_prem_tac
1997-11-07 oheimb 1997-11-07 changed libraray function find to find_index_eq, currying it
1997-11-03 wenzelm 1997-11-03 adapted to new implicit simpset;
1997-10-17 paulson 1997-10-17 New simprules imp_disj1,2 and some comments
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-08-06 berghofe 1997-08-06 Moved functions from file "thy_data.ML".
1997-07-23 wenzelm 1997-07-23 standard congs;
1997-07-22 paulson 1997-07-22 Removal of the tactical STATE
1997-05-15 oheimb 1997-05-15 renamed addss to addSss, unsafe_addss to addss, extended auto_tac
1997-03-18 nipkow 1997-03-18 Added P&P&Q <-> P&Q and P|P|Q <-> P|Q
1997-03-05 paulson 1997-03-05 Eta-expanded declarations of addSIs2, etc., to avoid polymorphism errors
1997-02-15 oheimb 1997-02-15 added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss, safe_asm_more_full_simp_tac new addss (old version retained as unsafe_addss), new auto_tac (old version retained as unsafe_auto_tac), clasimpset with modification functions
1997-02-10 paulson 1997-02-10 Renamed structure Int (intuitionistic prover) to IntPr to prevent clash with Basis Library structure Int
1997-01-03 paulson 1997-01-03 Implicit simpsets and clasets for FOL and ZF