diff -r bb18eed53ed6 -r a1119cf551e8 src/HOL/IMP/Sec_Typing.thy
--- a/src/HOL/IMP/Sec_Typing.thy	Tue Aug 13 14:20:22 2013 +0200
+++ b/src/HOL/IMP/Sec_Typing.thy	Tue Aug 13 16:25:47 2013 +0200
@@ -11,9 +11,9 @@
 Assign:
   "\<lbrakk> sec x \<ge> sec a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" |
 Seq:
-  "\<lbrakk> l \<turnstile> c\<^isub>1;  l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> c\<^isub>1;;c\<^isub>2" |
+  "\<lbrakk> l \<turnstile> c\<^sub>1;  l \<turnstile> c\<^sub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> c\<^sub>1;;c\<^sub>2" |
 If:
-  "\<lbrakk> max (sec b) l \<turnstile> c\<^isub>1;  max (sec b) l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2" |
+  "\<lbrakk> max (sec b) l \<turnstile> c\<^sub>1;  max (sec b) l \<turnstile> c\<^sub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> IF b THEN c\<^sub>1 ELSE c\<^sub>2" |
 While:
   "max (sec b) l \<turnstile> c \<Longrightarrow> l \<turnstile> WHILE b DO c"
 
@@ -24,7 +24,7 @@
 value "2 \<turnstile> IF Less (V ''x1'') (V ''x'') THEN ''x1'' ::= N 0 ELSE SKIP"
 
 inductive_cases [elim!]:
-  "l \<turnstile> x ::= a"  "l \<turnstile> c\<^isub>1;;c\<^isub>2"  "l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2"  "l \<turnstile> WHILE b DO c"
+  "l \<turnstile> x ::= a"  "l \<turnstile> c\<^sub>1;;c\<^sub>2"  "l \<turnstile> IF b THEN c\<^sub>1 ELSE c\<^sub>2"  "l \<turnstile> WHILE b DO c"
 
 
 text{* An important property: anti-monotonicity. *}
@@ -187,9 +187,9 @@
 Assign':
   "\<lbrakk> sec x \<ge> sec a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a" |
 Seq':
-  "\<lbrakk> l \<turnstile>' c\<^isub>1;  l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' c\<^isub>1;;c\<^isub>2" |
+  "\<lbrakk> l \<turnstile>' c\<^sub>1;  l \<turnstile>' c\<^sub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' c\<^sub>1;;c\<^sub>2" |
 If':
-  "\<lbrakk> sec b \<le> l;  l \<turnstile>' c\<^isub>1;  l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' IF b THEN c\<^isub>1 ELSE c\<^isub>2" |
+  "\<lbrakk> sec b \<le> l;  l \<turnstile>' c\<^sub>1;  l \<turnstile>' c\<^sub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' IF b THEN c\<^sub>1 ELSE c\<^sub>2" |
 While':
   "\<lbrakk> sec b \<le> l;  l \<turnstile>' c \<rbrakk> \<Longrightarrow> l \<turnstile>' WHILE b DO c" |
 anti_mono':
@@ -221,10 +221,10 @@
 Assign2:
   "sec x \<ge> sec a \<Longrightarrow> \<turnstile> x ::= a : sec x" |
 Seq2:
-  "\<lbrakk> \<turnstile> c\<^isub>1 : l\<^isub>1;  \<turnstile> c\<^isub>2 : l\<^isub>2 \<rbrakk> \<Longrightarrow> \<turnstile> c\<^isub>1;;c\<^isub>2 : min l\<^isub>1 l\<^isub>2 " |
+  "\<lbrakk> \<turnstile> c\<^sub>1 : l\<^sub>1;  \<turnstile> c\<^sub>2 : l\<^sub>2 \<rbrakk> \<Longrightarrow> \<turnstile> c\<^sub>1;;c\<^sub>2 : min l\<^sub>1 l\<^sub>2 " |
 If2:
-  "\<lbrakk> sec b \<le> min l\<^isub>1 l\<^isub>2;  \<turnstile> c\<^isub>1 : l\<^isub>1;  \<turnstile> c\<^isub>2 : l\<^isub>2 \<rbrakk>
-  \<Longrightarrow> \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2 : min l\<^isub>1 l\<^isub>2" |
+  "\<lbrakk> sec b \<le> min l\<^sub>1 l\<^sub>2;  \<turnstile> c\<^sub>1 : l\<^sub>1;  \<turnstile> c\<^sub>2 : l\<^sub>2 \<rbrakk>
+  \<Longrightarrow> \<turnstile> IF b THEN c\<^sub>1 ELSE c\<^sub>2 : min l\<^sub>1 l\<^sub>2" |
 While2:
   "\<lbrakk> sec b \<le> l;  \<turnstile> c : l \<rbrakk> \<Longrightarrow> \<turnstile> WHILE b DO c : l"