--- 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;