--- a/src/HOL/IMP/Collecting.thy Tue Feb 12 21:35:40 2013 +0100
+++ b/src/HOL/IMP/Collecting.thy Wed Feb 13 09:04:47 2013 +0100
@@ -142,14 +142,14 @@
subsubsection "Collecting semantics"
fun step :: "state set \<Rightarrow> state set acom \<Rightarrow> state set acom" where
-"step S (SKIP {P}) = (SKIP {S})" |
-"step S (x ::= e {P}) =
+"step S (SKIP {Q}) = (SKIP {S})" |
+"step S (x ::= e {Q}) =
x ::= e {{s(x := aval e s) |s. s : S}}" |
"step S (C1; C2) = step S C1; step (post C1) C2" |
-"step S (IF b THEN {P1} C1 ELSE {P2} C2 {P}) =
+"step S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
IF b THEN {{s:S. bval b s}} step P1 C1 ELSE {{s:S. \<not> bval b s}} step P2 C2
{post C1 \<union> post C2}" |
-"step S ({I} WHILE b DO {P} C {P'}) =
+"step S ({I} WHILE b DO {P} C {Q}) =
{S \<union> post C} WHILE b DO {{s:I. bval b s}} step P C {{s:I. \<not> bval b s}}"
definition CS :: "com \<Rightarrow> state set acom" where