# HG changeset patch
# User huffman
# Date 1313618610 25200
# Node ID e44f465c00a18439e3b6e496fc16823515e78e7f
# Parent  7784fa3232cec5fa086a8f64bdf48d60d30d7a87
HOL-IMP: respect set/pred distinction

diff -r 7784fa3232ce -r e44f465c00a1 src/HOL/IMP/Sem_Equiv.thy
--- a/src/HOL/IMP/Sem_Equiv.thy	Wed Aug 17 15:02:17 2011 -0700
+++ b/src/HOL/IMP/Sem_Equiv.thy	Wed Aug 17 15:03:30 2011 -0700
@@ -132,7 +132,7 @@
                simp: hoare_valid_def)
 
 lemma equiv_up_to_if:
-  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<inter> bval b \<Turnstile> c \<sim> c' \<Longrightarrow> (\<lambda>s. P s \<and> \<not>bval b s) \<Turnstile> d \<sim> d' \<Longrightarrow>
+  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow> (\<lambda>s. P s \<and> \<not>bval b s) \<Turnstile> d \<sim> d' \<Longrightarrow>
    P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'"
   by (auto simp: bequiv_up_to_def equiv_up_to_def)
 
@@ -162,4 +162,4 @@
   by (blast dest: while_never)
 
 
-end
\ No newline at end of file
+end