src/HOL/simpdata.ML
2001-11-23 wenzelm 2001-11-23 tuned;
2001-11-03 wenzelm 2001-11-03 proper use of bind_thm(s);
2001-10-04 wenzelm 2001-10-04 removed hol_rewrite_cterm (use full_rewrite_cterm from Pure);
2001-09-28 berghofe 2001-09-28 mksimps and mk_eq_True no longer raise THM exception.
2001-08-31 berghofe 2001-08-31 Proof of True_implies_equals is stored with "open" derivation to facilitate simplification of proof terms.
2001-07-25 paulson 2001-07-25 partial restructuring to reduce dependence on Axiom of Choice
2001-07-20 wenzelm 2001-07-20 HOL_ss: the_eq_trivial, the_sym_eq_trivial;
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
2001-03-23 nipkow 2001-03-23 added one point simprocs for bounded quantifiers
2001-03-09 nipkow 2001-03-09 arith_tac now copes with propositional reasoning as well.
2001-02-20 oheimb 2001-02-20 debugging: replaced gen_all by forall_elim_vars_safe
2001-02-02 wenzelm 2001-02-02 added hol_simplify, hol_rewrite_cterm;
2001-01-30 oheimb 2001-01-30 added if_def2
2000-10-17 paulson 2000-10-17 renaming of contrapos rules
2000-09-15 paulson 2000-09-15 renamed (most of...) the select rules
2000-09-07 wenzelm 2000-09-07 eliminated rulify setup (now in Provers/rulify.ML);
2000-09-06 wenzelm 2000-09-06 tuned;
2000-09-06 nipkow 2000-09-06 imp_cong bound at thm level.
2000-09-05 wenzelm 2000-09-05 iff declarations moved to clasimp.ML;
2000-09-04 wenzelm 2000-09-04 added safe_mk_meta_eq;
2000-09-02 wenzelm 2000-09-02 added 'iff del' att;
2000-08-30 nipkow 2000-08-30 Fixed rulify. As a result ?-vars in some recdef induction schemas were renamed.
2000-08-29 wenzelm 2000-08-29 cong setup now part of Simplifier;
2000-08-03 paulson 2000-08-03 new theorem neq_commute
2000-07-18 wenzelm 2000-07-18 * HOL: removed obsolete expand_if = split_if; theorems if_splits = split_if split_if_asm;
2000-06-28 paulson 2000-06-28 make_elim -> cla_make_elim; tidied
2000-06-02 oheimb 2000-06-02 added eta_contract_eq, also to simpset
2000-05-24 paulson 2000-05-24 installing the plus_ac0 simprules
2000-03-31 wenzelm 2000-03-31 added cong atts;
2000-03-31 wenzelm 2000-03-31 change_global/local_css move to Provers/clasimp.ML; fixed 'iff' att syntax; added 'cong' att;
2000-03-15 wenzelm 2000-03-15 splitter setup;
2000-01-07 paulson 2000-01-07 tidied parentheses
1999-10-05 berghofe 1999-10-05 Rule not_not is now stored in theory (needed by Inductive).
1999-09-29 wenzelm 1999-09-29 bind_thms;
1999-09-28 paulson 1999-09-28 AC rules for equality
1999-09-23 paulson 1999-09-23 tidied; added lemma restrict_to_left
1999-09-21 nipkow 1999-09-21 Mod because of new solver interface.
1999-08-26 wenzelm 1999-08-26 iff_attrib_setup;
1999-08-25 wenzelm 1999-08-25 proper bootstrap of HOL theory and packages;
1999-08-16 oheimb 1999-08-16 re-added refl in safe_solver
1999-07-29 paulson 1999-07-29 added parentheses to cope with a possible reduction of the precedence of unary minus
1999-07-19 paulson 1999-07-19 getting rid of qed_goal
1999-07-10 wenzelm 1999-07-10 handle THM/TERM exn;
1999-07-08 paulson 1999-07-08 Now if_weak_cong is a standard congruence rule
1999-04-27 wenzelm 1999-04-27 "iff" attribute; simpdata_setup;
1999-03-17 wenzelm 1999-03-17 Theory.sign_of;
1999-03-03 paulson 1999-03-03 expandshort
1999-03-01 paulson 1999-03-01 simpler proofs of congruence rules
1999-01-14 nipkow 1999-01-14 More arith refinements.
1998-11-26 nipkow 1998-11-26 Added a general refutation tactic which works by putting things into nnf first.
1998-09-24 oheimb 1998-09-24 simplified CLASIMP_DATA renamed mk_meta_eq to mk_eq, meta_eq to mk_meta_eq
1998-09-09 nipkow 1998-09-09 Proved and added rewrite rule (@x. x=y) = y to simpset. Strange that only the symetric version was present!
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-08-06 paulson 1998-08-06 even more tidying of Goal commands
1998-07-30 wenzelm 1998-07-30 made SML/NJ happy;
1998-07-30 wenzelm 1998-07-30 functorized Clasimp module;
1998-07-24 berghofe 1998-07-24 Added functions addIffs and delIffs which operate on clasimpsets.
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