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