1.1 --- a/src/HOL/IMP/Sem_Equiv.thy	Fri May 17 02:57:00 2013 +0200
     1.2 +++ b/src/HOL/IMP/Sem_Equiv.thy	Fri May 17 08:19:52 2013 +0200
     1.3 @@ -70,7 +70,7 @@
     1.4  lemma equiv_up_to_seq:
     1.5    "P \<Turnstile> c \<sim> c' \<Longrightarrow> Q \<Turnstile> d \<sim> d' \<Longrightarrow>
     1.6    (\<And>s s'. (c,s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> Q s') \<Longrightarrow>
     1.7 -  P \<Turnstile> (c; d) \<sim> (c'; d')"
     1.8 +  P \<Turnstile> (c;; d) \<sim> (c';; d')"
     1.9    by (clarsimp simp: equiv_up_to_def) blast
    1.10  
    1.11  lemma equiv_up_to_while_lemma: