src/HOL/simpdata.ML
2005-10-17 wenzelm 2005-10-17 change_claset/simpset; Simplifier.inherit_context instead of Simplifier.inherit_bounds;
2005-10-07 nipkow 2005-10-07 changes due to new neq_simproc in simpdata.ML
2005-09-12 haftmann 2005-09-12 introduced new-style AList operations
2005-08-31 wenzelm 2005-08-31 simp_implies: proper named infix;
2005-08-02 wenzelm 2005-08-02 added unfold_tac (Simplifier.inherit_bounds);
2005-08-02 ballarin 2005-08-02 Turned simp_implies into binary operator.
2005-07-01 berghofe 2005-07-01 Implemented trick (due to Tobias Nipkow) for fine-tuning simplification of premises of congruence rules.
2005-06-28 paulson 2005-06-28 Constant "If" is now local
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-12-18 schirmer 2004-12-18 added simproc for Let
2004-09-06 nipkow 2004-09-06 made mult_mono_thms generic.
2004-05-14 paulson 2004-05-14 new atomize theorem
2004-03-04 paulson 2004-03-04 new material from Avigad, and simplified treatment of division by 0
2002-12-09 ballarin 2002-12-09 Fixed bug in simpdata.ML that prevented the use of congruence rules from a locale. (mk_meta_cong did wrongly convert metahyps to hyps)
2002-09-30 berghofe 2002-09-30 Removed nRS again because extract_rews now takes care of preserving names.
2002-09-19 nipkow 2002-09-19 preserve names of rewrite rules when transforming them
2002-08-06 wenzelm 2002-08-06 sane interface for simprocs;
2002-02-28 paulson 2002-02-28 fixing nat_combine_numerals simprocs (again) Theorem eq_cong2 moved from Integ/int_arith1.ML to simpdata.ML, where it will be available in all theories. Function simplify_meta_eq now makes the meta-equality first so that eq_cong2 will work properly.
2002-01-12 wenzelm 2002-01-12 renamed forall_elim_vars_safe to gen_all;
2001-12-17 nipkow 2001-12-17 mods due to mor powerful simprocs for 1-point rules (quantifier1).
2001-12-12 nipkow 2001-12-12 Removed pointless backtracking from arith_tac
2001-11-24 wenzelm 2001-11-24 converted simp lemmas;
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