diff -r daac447f0e93 -r a6e3a5ec9847 src/HOL/IMP/Sec_TypingT.thy
--- a/src/HOL/IMP/Sec_TypingT.thy	Mon Mar 18 14:47:20 2013 +0100
+++ b/src/HOL/IMP/Sec_TypingT.thy	Mon Mar 18 19:20:53 2013 +0100
@@ -184,7 +184,8 @@
 anti_mono':
   "\<lbrakk> l \<turnstile>' c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c"
 
-lemma "l \<turnstile> c \<Longrightarrow> l \<turnstile>' c"
+lemma sec_type_sec_type': 
+  "l \<turnstile> c \<Longrightarrow> l \<turnstile>' c"
 apply(induction rule: sec_type.induct)
 apply (metis Skip')
 apply (metis Assign')
@@ -193,7 +194,8 @@
 by (metis While')
 
 
-lemma "l \<turnstile>' c \<Longrightarrow> l \<turnstile> c"
+lemma sec_type'_sec_type:
+  "l \<turnstile>' c \<Longrightarrow> l \<turnstile> c"
 apply(induction rule: sec_type'.induct)
 apply (metis Skip)
 apply (metis Assign)
@@ -202,4 +204,7 @@
 apply (metis While)
 by (metis anti_mono)
 
+corollary sec_type_eq: "l \<turnstile> c \<longleftrightarrow> l \<turnstile>' c"
+by (metis sec_type'_sec_type sec_type_sec_type')
+
 end