src/FOL/simpdata.ML
changeset 4930 89271bc4e7ed
parent 4794 9db0916ecdae
child 5115 caf39b7b7a12
     1.1 --- a/src/FOL/simpdata.ML	Thu May 14 16:44:04 1998 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Thu May 14 16:50:09 1998 +0200
     1.3 @@ -264,13 +264,20 @@
     1.4  fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
     1.5  fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
     1.6  
     1.7 -infix 4 addsplits;
     1.8 +infix 4 addsplits delsplits;
     1.9  fun ss addsplits splits =
    1.10 -  let fun addsplit(ss,split) =
    1.11 -        let val name = "split " ^ const_of_split_thm split
    1.12 -        in ss addloop (name,split_tac [split]) end
    1.13 +  let fun addsplit (ss,split) =
    1.14 +        let val (name,asm) = split_thm_info split 
    1.15 +        in ss addloop (name ^ (if asm then " asm" else ""),
    1.16 +		       (if asm then split_asm_tac else split_tac) [split]) end
    1.17    in foldl addsplit (ss,splits) end;
    1.18  
    1.19 +fun ss delsplits splits =
    1.20 +  let fun delsplit(ss,split) =
    1.21 +        let val (name,asm) = split_thm_info split 
    1.22 +        in ss delloop (name ^ (if asm then " asm" else "")) end
    1.23 +  in foldl delsplit (ss,splits) end;
    1.24 +
    1.25  val IFOL_simps =
    1.26     [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
    1.27      imp_simps @ iff_simps @ quant_simps;