src/HOL/IMP/Sec_Type_Expr.thy

--- a/src/HOL/IMP/Sec_Type_Expr.thy	Tue Aug 13 14:20:22 2013 +0200
+++ b/src/HOL/IMP/Sec_Type_Expr.thy	Tue Aug 13 16:25:47 2013 +0200
@@ -29,7 +29,7 @@
 fun sec_aexp :: "aexp \<Rightarrow> level" where
 "sec (N n) = 0" |
 "sec (V x) = sec x" |
-"sec (Plus a\<^isub>1 a\<^isub>2) = max (sec a\<^isub>1) (sec a\<^isub>2)"
+"sec (Plus a\<^sub>1 a\<^sub>2) = max (sec a\<^sub>1) (sec a\<^sub>2)"
 
 instance ..
 
@@ -41,8 +41,8 @@
 fun sec_bexp :: "bexp \<Rightarrow> level" where
 "sec (Bc v) = 0" |
 "sec (Not b) = sec b" |
-"sec (And b\<^isub>1 b\<^isub>2) = max (sec b\<^isub>1) (sec b\<^isub>2)" |
-"sec (Less a\<^isub>1 a\<^isub>2) = max (sec a\<^isub>1) (sec a\<^isub>2)"
+"sec (And b\<^sub>1 b\<^sub>2) = max (sec b\<^sub>1) (sec b\<^sub>2)" |
+"sec (Less a\<^sub>1 a\<^sub>2) = max (sec a\<^sub>1) (sec a\<^sub>2)"
 
 instance ..
 
@@ -58,11 +58,11 @@
 "s = s' (< l) == (\<forall> x. sec x < l \<longrightarrow> s x = s' x)"
 
 lemma aval_eq_if_eq_le:
-  "\<lbrakk> s\<^isub>1 = s\<^isub>2 (\<le> l);  sec a \<le> l \<rbrakk> \<Longrightarrow> aval a s\<^isub>1 = aval a s\<^isub>2"
+  "\<lbrakk> s\<^sub>1 = s\<^sub>2 (\<le> l);  sec a \<le> l \<rbrakk> \<Longrightarrow> aval a s\<^sub>1 = aval a s\<^sub>2"
 by (induct a) auto
 
 lemma bval_eq_if_eq_le:
-  "\<lbrakk> s\<^isub>1 = s\<^isub>2 (\<le> l);  sec b \<le> l \<rbrakk> \<Longrightarrow> bval b s\<^isub>1 = bval b s\<^isub>2"
+  "\<lbrakk> s\<^sub>1 = s\<^sub>2 (\<le> l);  sec b \<le> l \<rbrakk> \<Longrightarrow> bval b s\<^sub>1 = bval b s\<^sub>2"
 by (induct b) (auto simp add: aval_eq_if_eq_le)
 
 end