1.1 --- a/src/HOL/IMP/Collecting.thy	Tue Feb 12 21:35:40 2013 +0100
     1.2 +++ b/src/HOL/IMP/Collecting.thy	Wed Feb 13 09:04:47 2013 +0100
     1.3 @@ -142,14 +142,14 @@
     1.4  subsubsection "Collecting semantics"
     1.5  
     1.6  fun step :: "state set \<Rightarrow> state set acom \<Rightarrow> state set acom" where
     1.7 -"step S (SKIP {P}) = (SKIP {S})" |
     1.8 -"step S (x ::= e {P}) =
     1.9 +"step S (SKIP {Q}) = (SKIP {S})" |
    1.10 +"step S (x ::= e {Q}) =
    1.11    x ::= e {{s(x := aval e s) |s. s : S}}" |
    1.12  "step S (C1; C2) = step S C1; step (post C1) C2" |
    1.13 -"step S (IF b THEN {P1} C1 ELSE {P2} C2 {P}) =
    1.14 +"step S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
    1.15    IF b THEN {{s:S. bval b s}} step P1 C1 ELSE {{s:S. \<not> bval b s}} step P2 C2
    1.16    {post C1 \<union> post C2}" |
    1.17 -"step S ({I} WHILE b DO {P} C {P'}) =
    1.18 +"step S ({I} WHILE b DO {P} C {Q}) =
    1.19    {S \<union> post C} WHILE b DO {{s:I. bval b s}} step P C {{s:I. \<not> bval b s}}"
    1.20  
    1.21  definition CS :: "com \<Rightarrow> state set acom" where