--- a/src/FOL/simpdata.ML Fri Nov 28 10:52:32 1997 +0100
+++ b/src/FOL/simpdata.ML Fri Nov 28 10:54:13 1997 +0100
@@ -186,6 +186,8 @@
val split_asm_tac = mk_case_split_asm_tac split_tac
(disjE,conjE,exE,contrapos,contrapos2,notnotD);
+
+
(*** Standard simpsets ***)
structure Induction = InductionFun(struct val spec=IFOL.spec end);
@@ -202,6 +204,9 @@
fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
+infix 4 addsplits;
+fun ss addsplits splits = ss addloop (split_tac splits);
+
val IFOL_simps =
[refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @
imp_simps @ iff_simps @ quant_simps;