diff -r ec46a485bf60 -r 55908a74065f src/HOL/IMP/VCG.thy
--- a/src/HOL/IMP/VCG.thy	Tue Jun 11 21:24:12 2013 -0700
+++ b/src/HOL/IMP/VCG.thy	Wed Jun 12 13:53:24 2013 +0200
@@ -42,8 +42,8 @@
 "vc (C\<^isub>1;; C\<^isub>2) Q = (\<lambda>s. vc C\<^isub>1 (pre C\<^isub>2 Q) s \<and> vc C\<^isub>2 Q s)" |
 "vc (IF b THEN C\<^isub>1 ELSE C\<^isub>2) Q = (\<lambda>s. vc C\<^isub>1 Q s \<and> vc C\<^isub>2 Q s)" |
 "vc ({I} WHILE b DO C) Q =
-  (\<lambda>s. (I s \<and> \<not> bval b s \<longrightarrow> Q s) \<and>
-       (I s \<and> bval b s \<longrightarrow> pre C I s) \<and>
+  (\<lambda>s. (I s \<and> bval b s \<longrightarrow> pre C I s) \<and>
+       (I s \<and> \<not> bval b s \<longrightarrow> Q s) \<and>
        vc C I s)"