Splitters via named loopers.
authornipkow
Sat Feb 28 15:41:17 1998 +0100 (1998-02-28)
changeset 466906f3c56dcba8
parent 4668 131989b78417
child 4670 f309259fa828
Splitters via named loopers.
src/FOL/simpdata.ML
src/HOL/simpdata.ML
     1.1 --- a/src/FOL/simpdata.ML	Sat Feb 28 15:40:50 1998 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Sat Feb 28 15:41:17 1998 +0100
     1.3 @@ -267,7 +267,11 @@
     1.4  fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
     1.5  
     1.6  infix 4 addsplits;
     1.7 -fun ss addsplits splits = ss addloop (split_tac splits);
     1.8 +fun ss addsplits splits =
     1.9 +  let fun addsplit(ss,split) =
    1.10 +        let val name = "split " ^ const_of_split_thm split
    1.11 +        in ss addloop (name,split_tac [split]) end
    1.12 +  in foldl addsplit (ss,splits) end;
    1.13  
    1.14  val IFOL_simps =
    1.15     [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
     2.1 --- a/src/HOL/simpdata.ML	Sat Feb 28 15:40:50 1998 +0100
     2.2 +++ b/src/HOL/simpdata.ML	Sat Feb 28 15:41:17 1998 +0100
     2.3 @@ -337,8 +337,11 @@
     2.4  			(disjE,conjE,exE,contrapos,contrapos2,notnotD);
     2.5  
     2.6  infix 4 addsplits;
     2.7 -fun ss addsplits splits = ss addloop (split_tac splits);
     2.8 -
     2.9 +fun ss addsplits splits =
    2.10 +  let fun addsplit(ss,split) =
    2.11 +        let val name = "split " ^ const_of_split_thm split
    2.12 +        in ss addloop (name,split_tac [split]) end
    2.13 +  in foldl addsplit (ss,splits) end;
    2.14  
    2.15  qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
    2.16    (K [split_tac [expand_if] 1, blast_tac HOL_cs 1]);