src/HOL/simpdata.ML
2000-09-05 ago iff declarations moved to clasimp.ML;
2000-09-04 ago added safe_mk_meta_eq;
2000-09-02 ago added 'iff del' att;
2000-08-30 ago Fixed rulify.
2000-08-29 ago cong setup now part of Simplifier;
2000-08-03 ago new theorem neq_commute
2000-07-18 ago * HOL: removed obsolete expand_if = split_if; theorems if_splits =
2000-06-28 ago make_elim -> cla_make_elim; tidied
2000-06-02 ago added eta_contract_eq, also to simpset
2000-05-24 ago installing the plus_ac0 simprules
2000-03-31 ago added cong atts;
2000-03-31 ago change_global/local_css move to Provers/clasimp.ML;
2000-03-15 ago splitter setup;
2000-01-07 ago tidied parentheses
1999-10-05 ago Rule not_not is now stored in theory (needed by Inductive).
1999-09-29 ago bind_thms;
1999-09-28 ago AC rules for equality
1999-09-23 ago tidied; added lemma restrict_to_left
1999-09-21 ago Mod because of new solver interface.
1999-08-26 ago iff_attrib_setup;
1999-08-25 ago proper bootstrap of HOL theory and packages;
1999-08-16 ago re-added refl in safe_solver
1999-07-29 ago added parentheses to cope with a possible reduction of the precedence of unary
1999-07-19 ago getting rid of qed_goal
1999-07-10 ago handle THM/TERM exn;
1999-07-08 ago Now if_weak_cong is a standard congruence rule
1999-04-27 ago "iff" attribute;
1999-03-17 ago Theory.sign_of;
1999-03-03 ago expandshort
1999-03-01 ago simpler proofs of congruence rules
1999-01-14 ago More arith refinements.
1998-11-26 ago Added a general refutation tactic which works by putting things into nnf first.
1998-09-24 ago simplified CLASIMP_DATA
1998-09-09 ago Proved and added rewrite rule (@x. x=y) = y to simpset.
1998-08-12 ago minor adaption for SML/NJ
1998-08-12 ago the splitter is now defined as a functor
1998-08-06 ago even more tidying of Goal commands
1998-07-30 ago made SML/NJ happy;
1998-07-30 ago functorized Clasimp module;
1998-07-24 ago Added functions addIffs and delIffs which operate on clasimpsets.
1998-05-14 ago extended addsplits and delsplits to handle also split rules for assumptions
1998-04-27 ago Added a few lemmas.
1998-04-04 ago no open Simplifier;
1998-04-02 ago changed if_bool_eq to if_bool_eq_conj and added if_bool_eq_disj
1998-03-13 ago moved addsplits [expand_if] from HOL_basic_ss to HOL_ss;
1998-03-12 ago renamed not1_or to disj_not1, not2_or to disj_not2
1998-03-10 ago new rewrite rules not1_or, not2_or, and if_eq_cancel
1998-03-06 ago expand_if is now by default part of the simpset.
1998-03-04 ago Reorganized simplifier. May now reorient rules.
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
1998-02-20 ago Congruence rules use == in premises now.
1998-02-18 ago corrected problem with auto_tac: now uses a variant of depth_tac that avoids
1998-01-08 ago replaced fn _ => by K
1997-12-24 ago New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-12-03 ago Tidying and some comments
1997-11-28 ago Added comments
1997-11-28 ago Removed dead code.
1997-11-28 ago Moved the quantifier elimination simp procs into Provers.