--- a/src/HOL/IMP/Hoare.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/IMP/Hoare.ML Sat Mar 07 16:29:29 1998 +0100
@@ -61,13 +61,13 @@
(*Not suitable for rewriting: LOOPS!*)
goal Hoare.thy "wp (WHILE b DO c) Q s = \
\ (if b s then wp (c;WHILE b DO c) Q s else Q s)";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
qed "wp_While_if";
goal thy
"wp (WHILE b DO c) Q s = \
\ (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
by (rtac iffI 1);
by (rtac weak_coinduct 1);
by (etac CollectI 1);