1.1 --- a/src/HOL/IMP/Sem_Equiv.thy	Wed Aug 17 15:02:17 2011 -0700
     1.2 +++ b/src/HOL/IMP/Sem_Equiv.thy	Wed Aug 17 15:03:30 2011 -0700
     1.3 @@ -132,7 +132,7 @@
     1.4                 simp: hoare_valid_def)
     1.5  
     1.6  lemma equiv_up_to_if:
     1.7 -  "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>
     1.8 +  "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>
     1.9     P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'"
    1.10    by (auto simp: bequiv_up_to_def equiv_up_to_def)
    1.11  
    1.12 @@ -162,4 +162,4 @@
    1.13    by (blast dest: while_never)
    1.14  
    1.15  
    1.16 -end
    1.17 \ No newline at end of file
    1.18 +end