# HG changeset patch
# User nipkow
# Date 1348735420 -7200
# Node ID c54d901d29467dab9337b761137f8c980131d0a7
# Parent  a115dda102512bf3f44f527ac825538309801610
tuned

diff -r a115dda10251 -r c54d901d2946 src/HOL/IMP/Collecting.thy
--- a/src/HOL/IMP/Collecting.thy	Thu Sep 27 10:20:38 2012 +0200
+++ b/src/HOL/IMP/Collecting.thy	Thu Sep 27 10:43:40 2012 +0200
@@ -144,11 +144,11 @@
 fun step :: "state set \<Rightarrow> state set acom \<Rightarrow> state set acom" where
 "step S (SKIP {P}) = (SKIP {S})" |
 "step S (x ::= e {P}) =
-  (x ::= e {{s'. EX s:S. s' = s(x := aval e s)}})" |
+  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}) =
-   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}" |
+  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'}) =
   {S \<union> post C} WHILE b DO {{s:I. bval b s}} step P C {{s:I. \<not> bval b s}}"