src/HOL/Tools/meson.ML
changeset 18752 c9c6ae9e8b88
parent 18708 4b3dadb4fe33
child 18817 ad8bc3e55aa3
     1.1 --- a/src/HOL/Tools/meson.ML	Mon Jan 23 11:37:53 2006 +0100
     1.2 +++ b/src/HOL/Tools/meson.ML	Mon Jan 23 11:38:43 2006 +0100
     1.3 @@ -142,7 +142,6 @@
     1.4  
     1.5  fun refl_clause_aux 0 th = th
     1.6    | refl_clause_aux n th =
     1.7 -(Output.debug ("refl_clause_aux " ^ Int.toString n ^ " " ^ string_of_thm th);
     1.8         case HOLogic.dest_Trueprop (concl_of th) of
     1.9  	  (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _) => 
    1.10              refl_clause_aux n (th RS disj_assoc)    (*isolate an atom as first disjunct*)
    1.11 @@ -152,7 +151,7 @@
    1.12  		 handle THM _ => refl_clause_aux (n-1) (th RS disj_comm))  (*ignore*)
    1.13  	    else refl_clause_aux (n-1) (th RS disj_comm)  (*not between Vars: ignore*)
    1.14  	| (Const ("op |", _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
    1.15 -	| _ => (*not a disjunction*) th);
    1.16 +	| _ => (*not a disjunction*) th;
    1.17  
    1.18  fun notequal_lits_count (Const ("op |", _) $ P $ Q) = 
    1.19        notequal_lits_count P + notequal_lits_count Q
    1.20 @@ -393,10 +392,9 @@
    1.21  
    1.22  val nnf_ss =
    1.23      HOL_basic_ss addsimps
    1.24 -     (nnf_simps @ [if_True, if_False, if_cancel, if_eq_cancel, cases_simp]
    1.25 -     @ ex_simps @ all_simps @ simp_thms)
    1.26 -     addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc]
    1.27 -     addsplits [split_if];
    1.28 +     (nnf_simps @ [if_True, if_False, if_cancel, if_eq_cancel, cases_simp] @
    1.29 +      thms"split_ifs" @ ex_simps @ all_simps @ simp_thms)
    1.30 +     addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc];
    1.31  
    1.32  fun make_nnf th = th |> simplify nnf_ss
    1.33                       |> make_nnf1