# HG changeset patch # User paulson # Date 1134573266 -3600 # Node ID afb1a52a7011e0472270413a5d5db60fd87d00ed # Parent aa27c10a040e955b4bb2541a37f9c63cf6b37a44 removal of some redundancies (e.g. one-point-rules) in clause production diff -r aa27c10a040e -r afb1a52a7011 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Wed Dec 14 16:13:09 2005 +0100 +++ b/src/HOL/Tools/meson.ML Wed Dec 14 16:14:26 2005 +0100 @@ -389,11 +389,19 @@ (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward])) handle THM _ => th; -(*The simplification removes defined quantifiers and occurrences of True and False, as well as tags applied to True and False.*) +(*The simplification removes defined quantifiers and occurrences of True and False, + as well as tags applied to True and False. nnf_ss also includes the one-point simprocs, + which are needed to avoid the various one-point theorems from generating junk clauses.*) val tag_True = thm "tag_True"; val tag_False = thm "tag_False"; val nnf_simps = [Ex1_def,Ball_def,Bex_def,tag_True,tag_False] -val nnf_ss = HOL_basic_ss addsimps nnf_simps@simp_thms; + +val nnf_ss = + HOL_basic_ss addsimps + (nnf_simps @ [if_True, if_False, if_cancel, if_eq_cancel, cases_simp] + @ ex_simps @ all_simps @ simp_thms) + addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc] + addsplits [split_if]; fun make_nnf th = th |> simplify nnf_ss |> make_nnf1