src/HOL/IMP/Sem_Equiv.thy
changeset 45218 f115540543d8
parent 45200 1f1897ac7877
child 47818 151d137f1095
     1.1 --- a/src/HOL/IMP/Sem_Equiv.thy	Thu Oct 20 10:44:00 2011 +0200
     1.2 +++ b/src/HOL/IMP/Sem_Equiv.thy	Thu Oct 20 12:30:43 2011 -0400
     1.3 @@ -43,7 +43,7 @@
     1.4    "(P \<Turnstile> c \<sim> c') = (P \<Turnstile> c' \<sim> c)"
     1.5    by (auto simp: equiv_up_to_def)
     1.6  
     1.7 -lemma equiv_up_to_trans [trans]:
     1.8 +lemma equiv_up_to_trans:
     1.9    "P \<Turnstile> c \<sim> c' \<Longrightarrow> P \<Turnstile> c' \<sim> c'' \<Longrightarrow> P \<Turnstile> c \<sim> c''"
    1.10    by (auto simp: equiv_up_to_def)
    1.11  
    1.12 @@ -56,7 +56,7 @@
    1.13    "(P \<Turnstile> b <\<sim>> b') = (P \<Turnstile> b' <\<sim>> b)"
    1.14    by (auto simp: bequiv_up_to_def)
    1.15  
    1.16 -lemma bequiv_up_to_trans [trans]:
    1.17 +lemma bequiv_up_to_trans:
    1.18    "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> b' <\<sim>> b'' \<Longrightarrow> P \<Turnstile> b <\<sim>> b''"
    1.19    by (auto simp: bequiv_up_to_def)
    1.20