# HG changeset patch
# User nipkow
# Date 1371038004 -7200
# Node ID 55908a74065fbefd501921a38e3db70fb6e246bb
# Parent  ec46a485bf60c001114d7a65959ee02c9200f324
same order of properties as in While rule

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)"