--- a/src/HOL/IMP/Hoare.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/IMP/Hoare.ML Fri Oct 10 19:02:28 1997 +0200
@@ -27,7 +27,7 @@
by (Simp_tac 1);
qed "wp_SKIP";
-goalw Hoare.thy [wp_def] "wp (x:=a) Q = (%s.Q(s[a s/x]))";
+goalw Hoare.thy [wp_def] "wp (x:=a) Q = (%s. Q(s[a s/x]))";
by (Simp_tac 1);
qed "wp_Ass";
@@ -66,7 +66,7 @@
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}))";
+\ (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))";
by (simp_tac (!simpset setloop(split_tac[expand_if])) 1);
by (rtac iffI 1);
by (rtac weak_coinduct 1);