src/HOL/simpdata.ML
2006-11-12 wenzelm 2006-11-12 mk_atomize: careful matching against rules admits overloading;
2006-11-03 haftmann 2006-11-03 re-added simpdata.ML
2006-10-16 haftmann 2006-10-16 slight cleanup
2006-10-11 haftmann 2006-10-11 cleaned up HOL bootstrap
2006-10-10 haftmann 2006-10-10 cleanup basic HOL bootstrap
2006-10-10 haftmann 2006-10-10 fixed typo
2006-10-07 wenzelm 2006-10-07 tuned;
2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs)
2006-07-11 wenzelm 2006-07-11 let_simproc: activate Variable.import;
2006-07-08 wenzelm 2006-07-08 Goal.prove_global;
2006-07-05 schirmer 2006-07-05 fixed let-simproc ----------------------------------------------------------------------
2006-04-26 wenzelm 2006-04-26 removed obsolete expand_case_tac;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2005-12-31 wenzelm 2005-12-31 removed obsolete Provers/make_elim.ML;
2005-12-14 paulson 2005-12-14 deleted redundant (looping!) simprule
2005-12-01 wenzelm 2005-12-01 unfold_tac: static evaluation of simpset;
2005-11-16 wenzelm 2005-11-16 Term.betapply;
2005-10-25 wenzelm 2005-10-25 avoid legacy goals;
2005-10-21 wenzelm 2005-10-21 OldGoals;
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-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);