# 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 \ (\i. v = Iv i)" +lemma type_eq_Ity[simp]: "type v = Ity \ (\i. v = Iv i)" by (cases v) simp_all -lemma [simp]: "type v = Rty \ (\r. v = Rv r)" +lemma type_eq_Rty[simp]: "type v = Rty \ (\r. v = Rv r)" by (cases v) simp_all definition styping :: "tyenv \ state \ bool" (infix "\" 50)