--- 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