diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Sem_Equiv.thy
--- a/src/HOL/IMP/Sem_Equiv.thy	Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Sem_Equiv.thy	Sat Apr 28 07:38:22 2012 +0200
@@ -70,7 +70,7 @@
   by (rule equiv_up_to_hoare)
 
 
-lemma equiv_up_to_semi:
+lemma equiv_up_to_seq:
   "P \<Turnstile> c \<sim> c' \<Longrightarrow> Q \<Turnstile> d \<sim> d' \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow>
   P \<Turnstile> (c; d) \<sim> (c'; d')"
   by (clarsimp simp: equiv_up_to_def hoare_valid_def) blast