src/HOL/simpdata.ML
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
1998-04-27 nipkow 1998-04-27 Added a few lemmas. Renamed expand_const -> split_const.
1998-04-04 wenzelm 1998-04-04 no open Simplifier;
1998-04-02 paulson 1998-04-02 changed if_bool_eq to if_bool_eq_conj and added if_bool_eq_disj
1998-03-13 wenzelm 1998-03-13 moved addsplits [expand_if] from HOL_basic_ss to HOL_ss;
1998-03-12 oheimb 1998-03-12 renamed not1_or to disj_not1, not2_or to disj_not2
1998-03-10 oheimb 1998-03-10 new rewrite rules not1_or, not2_or, and if_eq_cancel added not1_or and if_eq_cancel to simpset()
1998-03-06 nipkow 1998-03-06 expand_if is now by default part of the simpset.
1998-03-04 nipkow 1998-03-04 Reorganized simplifier. May now reorient rules.
1998-02-28 nipkow 1998-02-28 Splitters via named loopers.
1998-02-25 oheimb 1998-02-25 factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning combination of classical reasoner and simplifier auto_tac into Provers/clasimp.ML explicitly introducing combined type clasimpset
1998-02-25 oheimb 1998-02-25 changed wrapper mechanism of classical reasoner
1998-02-20 nipkow 1998-02-20 Congruence rules use == in premises now. New class linord.
1998-02-18 oheimb 1998-02-18 corrected problem with auto_tac: now uses a variant of depth_tac that avoids interference of the simplifier with dup_step_tac
1998-01-08 oheimb 1998-01-08 replaced fn _ => by K
1997-12-24 paulson 1997-12-24 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-12-03 paulson 1997-12-03 Tidying and some comments
1997-11-28 paulson 1997-11-28 Added comments
1997-11-28 nipkow 1997-11-28 Removed dead code.
1997-11-28 nipkow 1997-11-28 Moved the quantifier elimination simp procs into Provers.
1997-11-12 oheimb 1997-11-12 simpdata.ML: renamed split_prem_tac to split_asm_tac, added split_if_asm cladata.ML: unintentinally committed
1997-11-07 oheimb 1997-11-07 added split_prem_tac
1997-11-07 oheimb 1997-11-07 changed libraray function find to find_index_eq, currying it
1997-11-04 wenzelm 1997-11-04 removed old datatype_info;
1997-11-04 nipkow 1997-11-04 Logic.loops -> Logic.rewrite_rule_ok
1997-11-03 wenzelm 1997-11-03 adapted to new implicit simpset;
1997-10-30 nipkow 1997-10-30 For each datatype `t' there is now a theorem `split_t_case' of the form P(t_case f1 ... fn x) = ((!y1 ... ym1. x = C1 y1 ... ym1 --> P(f1 y1 ... ym1))& ... (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))) The simplifier now reduces !x. (..x.. & x = t & ..x..) --> P x to (..t.. & ..t..) --> P t (and similarly for t=x).
1997-10-17 nipkow 1997-10-17 setloop split_tac -> addsplits
1997-10-17 paulson 1997-10-17 New trivial rewrites
1997-10-16 paulson 1997-10-16 New simprules imp_disj1, imp_disj2
1997-10-16 nipkow 1997-10-16 Various new lemmas. Improved conversion of equations to rewrite rules: (s=t becomes (s=t)==True if s=t loops).
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-09-02 nipkow 1997-09-02 Added True_implies_equals
1997-08-06 berghofe 1997-08-06 Moved some functions which used to be part of thy_data.ML
1997-07-25 wenzelm 1997-07-25 added prems argument to simplification procedures;
1997-07-24 nipkow 1997-07-24 Deleted comment.
1997-07-24 nipkow 1997-07-24 List.ML: added lemmas by Stefan Merz. simpodata.ML: removed rules about ? now subsumed by simplification proc.
1997-07-23 nipkow 1997-07-23 Prod.ML: Added split_paired_EX and lots of comments about failed attempts to automate reasoning about products. simpdata.ML: added simplification procedure for simplifying existential statements of the form ? x. ... & x = t & ...
1997-07-23 wenzelm 1997-07-23 tuned congs: standard;
1997-07-22 paulson 1997-07-22 Removal of the tactical STATE
1997-07-14 paulson 1997-07-14 Fixed delIffs to deal correctly with the D-rule
1997-06-19 paulson 1997-06-19 Two new rewrite rules--NOT included by default\!
1997-06-18 paulson 1997-06-18 Addition of not_imp (which pushes negation into implication) as a default simprule
1997-05-22 nipkow 1997-05-22 Added exhaustion thm and exhaust_tac for each datatype.
1997-05-15 oheimb 1997-05-15 renamed addss to addSss, unsafe_addss to addss, extended auto_tac
1997-04-24 nipkow 1997-04-24 Introduced a generic "induct_tac" which picks up the right induction scheme automatically. Also changed nat_ind_tac, which does no longer append a "1" to the name of the induction variable. This caused some changes...
1997-04-15 paulson 1997-04-15 Moved expand_case_tac from Auth/Message.ML to simpdata.ML
1997-04-11 paulson 1997-04-11 Yet more fast_tac->blast_tac, and other tidying
1997-03-18 paulson 1997-03-18 Made the indentation rational
1997-03-18 nipkow 1997-03-18 Added P&P&Q = P&Q and P|P|Q = P|Q.
1997-03-07 paulson 1997-03-07 Eta-expanded some declarations for compatibility with value polymorphism
1997-03-04 paulson 1997-03-04 Renamed constant "not" to "Not"
1997-02-15 oheimb 1997-02-15 added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss, safe_asm_more_full_simp_ta, clasimpset HOL_css with modification functions new addss (old version retained as unsafe_addss), new Addss (old version retained as Unsafe_Addss), new auto_tac (old version retained as unsafe_auto_tac),
1997-02-07 nipkow 1997-02-07 Added "triv_forall_equality" to HOL_ss.
1996-12-18 oheimb 1996-12-18 factored out HOL_base_ss and val HOL_min_ss, added HOL_safe_min_ss
1996-11-27 oheimb 1996-11-27 moved split_tac