src/HOL/IMP/Sem_Equiv.thy
changeset 47818 151d137f1095
parent 45218 f115540543d8
child 48909 b2dea007e55e
     1.1 --- a/src/HOL/IMP/Sem_Equiv.thy	Fri Apr 27 23:17:58 2012 +0200
     1.2 +++ b/src/HOL/IMP/Sem_Equiv.thy	Sat Apr 28 07:38:22 2012 +0200
     1.3 @@ -70,7 +70,7 @@
     1.4    by (rule equiv_up_to_hoare)
     1.5  
     1.6  
     1.7 -lemma equiv_up_to_semi:
     1.8 +lemma equiv_up_to_seq:
     1.9    "P \<Turnstile> c \<sim> c' \<Longrightarrow> Q \<Turnstile> d \<sim> d' \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow>
    1.10    P \<Turnstile> (c; d) \<sim> (c'; d')"
    1.11    by (clarsimp simp: equiv_up_to_def hoare_valid_def) blast