src/HOL/simpdata.ML
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
1999-09-21 nipkow 1999-09-21 Mod because of new solver interface.
1999-08-26 wenzelm 1999-08-26 iff_attrib_setup;
1999-08-25 wenzelm 1999-08-25 proper bootstrap of HOL theory and packages;
1999-08-16 oheimb 1999-08-16 re-added refl in safe_solver
1999-07-29 paulson 1999-07-29 added parentheses to cope with a possible reduction of the precedence of unary minus
1999-07-19 paulson 1999-07-19 getting rid of qed_goal
1999-07-10 wenzelm 1999-07-10 handle THM/TERM exn;
1999-07-08 paulson 1999-07-08 Now if_weak_cong is a standard congruence rule
1999-04-27 wenzelm 1999-04-27 "iff" attribute; simpdata_setup;
1999-03-17 wenzelm 1999-03-17 Theory.sign_of;
1999-03-03 paulson 1999-03-03 expandshort
1999-03-01 paulson 1999-03-01 simpler proofs of congruence rules
1999-01-14 nipkow 1999-01-14 More arith refinements.
1998-11-26 nipkow 1998-11-26 Added a general refutation tactic which works by putting things into nnf first.
1998-09-24 oheimb 1998-09-24 simplified CLASIMP_DATA renamed mk_meta_eq to mk_eq, meta_eq to mk_meta_eq
1998-09-09 nipkow 1998-09-09 Proved and added rewrite rule (@x. x=y) = y to simpset. Strange that only the symetric version was present!
1998-08-12 oheimb 1998-08-12 minor adaption for SML/NJ
1998-08-12 oheimb 1998-08-12 the splitter is now defined as a functor moved addsplits, delsplits, Addsplits, Delsplits to Provers/splitter.ML moved split_thm_info to Provers/splitter.ML definined atomize via general mk_atomize removed superfluous rot_eq_tac from simplifier.ML HOL/simpdata.ML: renamed mk_meta_eq to meta_eq, re-renamed mk_meta_eq_simp to mk_meta_eq added Eps_eq to simpset
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