--- a/src/HOLCF/IOA/NTP/Correctness.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/NTP/Correctness.ML Mon Apr 27 16:47:50 1998 +0200
@@ -68,7 +68,7 @@
(* Proof of correctness *)
goalw Correctness.thy [Spec.ioa_def, is_weak_ref_map_def]
"is_weak_ref_map hom (restrict impl_ioa (externals spec_sig)) spec_ioa";
-by (simp_tac (simpset() delsplits [expand_if] addsimps
+by (simp_tac (simpset() delsplits [split_if] addsimps
[Correctness.hom_def, cancel_restrict, externals_lemma]) 1);
by (rtac conjI 1);
by (simp_tac ss' 1);
@@ -77,7 +77,7 @@
by (rtac imp_conj_lemma 1); (* from lemmas.ML *)
by (Action.action.induct_tac "a" 1);
-by (asm_simp_tac (ss' setloop (split_tac [expand_if])) 1);
+by (asm_simp_tac (ss' addsplits [split_if]) 1);
by (forward_tac [inv4] 1);
by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);
by (simp_tac ss' 1);