# HG changeset patch
# User nipkow
# Date 1385672621 -3600
# Node ID 6593e06445e67e7708131db599efbc9effc68049
# Parent  c71eb0537d37c8878a5be80f83618ac91a7f4524
tuned

diff -r c71eb0537d37 -r 6593e06445e6 src/HOL/IMP/Types.thy
--- a/src/HOL/IMP/Types.thy	Thu Nov 28 16:04:10 2013 +0100
+++ b/src/HOL/IMP/Types.thy	Thu Nov 28 22:03:41 2013 +0100
@@ -113,10 +113,10 @@
 "type (Iv i) = Ity" |
 "type (Rv r) = Rty"
 
-lemma [simp]: "type v = Ity \<longleftrightarrow> (\<exists>i. v = Iv i)"
+lemma type_eq_Ity[simp]: "type v = Ity \<longleftrightarrow> (\<exists>i. v = Iv i)"
 by (cases v) simp_all
 
-lemma [simp]: "type v = Rty \<longleftrightarrow> (\<exists>r. v = Rv r)"
+lemma type_eq_Rty[simp]: "type v = Rty \<longleftrightarrow> (\<exists>r. v = Rv r)"
 by (cases v) simp_all
 
 definition styping :: "tyenv \<Rightarrow> state \<Rightarrow> bool" (infix "\<turnstile>" 50)