# HG changeset patch
# User nipkow
# Date 1370523174 -7200
# Node ID cc5718f60778b0d6e16216510bd75dbda8031455
# Parent  fafab8eac3eeb45fe9ecd8b8f6e96a6c5fc80af6
tuned defs

diff -r fafab8eac3ee -r cc5718f60778 src/HOL/IMP/Hoare_Sound_Complete.thy
--- a/src/HOL/IMP/Hoare_Sound_Complete.thy	Thu Jun 06 12:16:35 2013 +0200
+++ b/src/HOL/IMP/Hoare_Sound_Complete.thy	Thu Jun 06 14:52:54 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 fafab8eac3ee -r cc5718f60778 src/HOL/IMP/VCG.thy
--- a/src/HOL/IMP/VCG.thy	Thu Jun 06 12:16:35 2013 +0200
+++ b/src/HOL/IMP/VCG.thy	Thu Jun 06 14:52:54 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: *}