# HG changeset patch
# User paulson
# Date 899394966 -7200
# Node ID caf39b7b7a126e30e08f5ee83456898ebe66ee25
# Parent  c729d4c299c1009816d4eb9d08a92ef5e126f68f
HACKED declaration of addsplits

diff -r c729d4c299c1 -r caf39b7b7a12 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Thu Jul 02 17:48:11 1998 +0200
+++ b/src/FOL/simpdata.ML	Thu Jul 02 17:56:06 1998 +0200
@@ -264,20 +264,36 @@
 fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
 fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
 
+(** FIXME: this is a PATCH until similar code in Provers/splitter is
+    generalized **)
+
+fun split_format_err() = error("Wrong format for split rule");
+
+fun split_thm_info thm =
+  (case concl_of thm of
+     Const("Trueprop",_) $ (Const("op <->", _)$(Var _$t)$c) =>
+        (case strip_comb t of
+           (Const(a,_),_) => (a,case c of (Const("Not",_)$_)=> true |_=> false)
+         | _              => split_format_err())
+   | _ => split_format_err());
+
 infix 4 addsplits delsplits;
 fun ss addsplits splits =
   let fun addsplit (ss,split) =
         let val (name,asm) = split_thm_info split 
-        in ss addloop (name ^ (if asm then " asm" else ""),
+        in ss addloop ("split "^ name ^ (if asm then " asm" else ""),
 		       (if asm then split_asm_tac else split_tac) [split]) end
   in foldl addsplit (ss,splits) end;
 
 fun ss delsplits splits =
   let fun delsplit(ss,split) =
         let val (name,asm) = split_thm_info split 
-        in ss delloop (name ^ (if asm then " asm" else "")) end
+        in ss delloop ("split "^ name ^ (if asm then " asm" else "")) end
   in foldl delsplit (ss,splits) end;
 
+fun Addsplits splits = (simpset_ref() := simpset() addsplits splits);
+fun Delsplits splits = (simpset_ref() := simpset() delsplits splits);
+
 val IFOL_simps =
    [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
     imp_simps @ iff_simps @ quant_simps;