1.1 --- a/src/HOL/IMP/Types.thy	Thu Nov 28 16:04:10 2013 +0100
     1.2 +++ b/src/HOL/IMP/Types.thy	Thu Nov 28 22:03:41 2013 +0100
     1.3 @@ -113,10 +113,10 @@
     1.4  "type (Iv i) = Ity" |
     1.5  "type (Rv r) = Rty"
     1.6  
     1.7 -lemma [simp]: "type v = Ity \<longleftrightarrow> (\<exists>i. v = Iv i)"
     1.8 +lemma type_eq_Ity[simp]: "type v = Ity \<longleftrightarrow> (\<exists>i. v = Iv i)"
     1.9  by (cases v) simp_all
    1.10  
    1.11 -lemma [simp]: "type v = Rty \<longleftrightarrow> (\<exists>r. v = Rv r)"
    1.12 +lemma type_eq_Rty[simp]: "type v = Rty \<longleftrightarrow> (\<exists>r. v = Rv r)"
    1.13  by (cases v) simp_all
    1.14  
    1.15  definition styping :: "tyenv \<Rightarrow> state \<Rightarrow> bool" (infix "\<turnstile>" 50)