src/HOL/simpdata.ML
1997-11-07 ago added split_prem_tac
1997-11-07 ago changed libraray function find to find_index_eq, currying it
1997-11-04 ago removed old datatype_info;
1997-11-04 ago Logic.loops -> Logic.rewrite_rule_ok
1997-11-03 ago adapted to new implicit simpset;
1997-10-30 ago For each datatype `t' there is now a theorem `split_t_case' of the form
1997-10-17 ago setloop split_tac -> addsplits
1997-10-17 ago New trivial rewrites
1997-10-16 ago New simprules imp_disj1, imp_disj2
1997-10-16 ago Various new lemmas. Improved conversion of equations to rewrite rules:
1997-10-10 ago fixed dots;
1997-09-02 ago Added True_implies_equals
1997-08-06 ago Moved some functions which used to be part of thy_data.ML
1997-07-25 ago added prems argument to simplification procedures;
1997-07-24 ago Deleted comment.
1997-07-24 ago List.ML: added lemmas by Stefan Merz.
1997-07-23 ago Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
1997-07-23 ago tuned congs: standard;
1997-07-22 ago Removal of the tactical STATE
1997-07-14 ago Fixed delIffs to deal correctly with the D-rule
1997-06-19 ago Two new rewrite rules--NOT included by default\!
1997-06-18 ago Addition of not_imp (which pushes negation into implication) as a default
1997-05-22 ago Added exhaustion thm and exhaust_tac for each datatype.
1997-05-15 ago renamed addss to addSss, unsafe_addss to addss, extended auto_tac
1997-04-24 ago Introduced a generic "induct_tac" which picks up the right induction scheme
1997-04-15 ago Moved expand_case_tac from Auth/Message.ML to simpdata.ML
1997-04-11 ago Yet more fast_tac->blast_tac, and other tidying
1997-03-18 ago Made the indentation rational
1997-03-18 ago Added P&P&Q = P&Q and P|P|Q = P|Q.
1997-03-07 ago Eta-expanded some declarations for compatibility with value polymorphism
1997-03-04 ago Renamed constant "not" to "Not"
1997-02-15 ago added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss,
1997-02-07 ago Added "triv_forall_equality" to HOL_ss.
1996-12-18 ago factored out HOL_base_ss and val HOL_min_ss, added HOL_safe_min_ss
1996-11-27 ago moved split_tac
1996-11-27 ago moved if_cancel to the right place
1996-11-27 ago added if_cancel later to simpset
1996-11-26 ago if_cancel added to HOL_ss
1996-10-28 ago Renamed and shuffled a few thms.
1996-10-25 ago Added (? x. t=x) = True
1996-10-15 ago corrected `correction` of o_assoc (of version 1.14),
1996-10-15 ago bound o_apply theorem to thy
1996-10-10 ago Addition of de Morgan laws
1996-10-07 ago New one-point rules for quantifiers
1996-09-26 ago Ran expandshort; used stac instead of ssubst
1996-09-26 ago Ran expandshort
1996-09-24 ago Fixed spelling error in comment
1996-09-12 ago Installed AddIffs, and some code from HOL.ML
1996-09-10 ago Beefed-up auto-tactic: now repeatedly simplifies if needed
1996-09-05 ago Added miniscoping to the simplifier: quantifiers are now pushed in
1996-08-19 ago Installation of auto_tac; re-organization
1996-07-29 ago Added two new distributive laws
1996-07-17 ago Corrected o_assoc lemma
1996-06-21 ago Added function Addss.
1996-05-22 ago Added ex_imp
1996-05-06 ago Added split_inside_tac.
1996-04-17 ago *** empty log message ***
1996-04-11 ago Added a number of lemmas
1996-03-06 ago Added 'section' commands
1996-02-09 ago Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'