# HG changeset patch
# User blanchet
# Date 1370526541 -7200
# Node ID e6ed134ecd16a9efef227233571c90a099bd9343
# Parent  7132de3059216ea8f7363db0d71c93d38afa6707# Parent  cc5718f60778b0d6e16216510bd75dbda8031455
merge

diff -r 7132de305921 -r e6ed134ecd16 src/HOL/IMP/Hoare_Sound_Complete.thy
--- a/src/HOL/IMP/Hoare_Sound_Complete.thy	Thu Jun 06 12:20:04 2013 +0200
+++ b/src/HOL/IMP/Hoare_Sound_Complete.thy	Thu Jun 06 15:49:01 2013 +0200
@@ -36,7 +36,7 @@
 
 lemma wp_If[simp]:
  "wp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) Q =
- (\<lambda>s. (bval b s \<longrightarrow> wp c\<^isub>1 Q s) \<and>  (\<not> bval b s \<longrightarrow> wp c\<^isub>2 Q s))"
+ (\<lambda>s. if bval b s then wp c\<^isub>1 Q s else wp c\<^isub>2 Q s)"
 by (rule ext) (auto simp: wp_def)
 
 lemma wp_While_If:
diff -r 7132de305921 -r e6ed134ecd16 src/HOL/IMP/VCG.thy
--- a/src/HOL/IMP/VCG.thy	Thu Jun 06 12:20:04 2013 +0200
+++ b/src/HOL/IMP/VCG.thy	Thu Jun 06 15:49:01 2013 +0200
@@ -31,8 +31,7 @@
 "pre (x ::= a) Q = (\<lambda>s. Q(s(x := aval a s)))" |
 "pre (c\<^isub>1;; c\<^isub>2) Q = pre c\<^isub>1 (pre c\<^isub>2 Q)" |
 "pre (IF b THEN c\<^isub>1 ELSE c\<^isub>2) Q =
-  (\<lambda>s. (bval b s \<longrightarrow> pre c\<^isub>1 Q s) \<and>
-       (\<not> bval b s \<longrightarrow> pre c\<^isub>2 Q s))" |
+  (\<lambda>s. if bval b s then pre c\<^isub>1 Q s else pre c\<^isub>2 Q s)" |
 "pre ({I} WHILE b DO c) Q = I"
 
 text{* Verification condition: *}