--- a/Paper.thy	Sun Jun 23 03:55:49 2013 +0100
+++ b/Paper.thy	Fri Sep 06 12:55:12 2013 +0100
@@ -91,9 +91,9 @@
   InheritParent_file_type ("InheritPatentType") and
   NormalFile_type ("NormalFileType") and
   deleted ("deleted _ _" [50, 100] 100) and
-  taintable_s ("taintable\<^isup>s") and
-  tainted_s ("tainted\<^isup>s") and
-  all_sobjs ("reachable\<^isup>s") and
+  taintable_s ("taintable\<^sup>s") and
+  tainted_s ("tainted\<^sup>s") and
+  all_sobjs ("reachable\<^sup>s") and
   init_obj2sobj ("\<lbrakk>_\<rbrakk>") and
   erole_functor ("erole'_aux") --"I have a erole_functor and etype_aux to handle 
                                  efficient, but their name not same, so ..., but don't work"
@@ -773,7 +773,7 @@
   potentially infinitely many of them and therefore the search space would be
   infinite.  For example starting from an
   initial state containing a process @{text p} and a file @{text pf}, 
-  we can create files @{text "f\<^isub>1"}, @{text "f\<^isub>2"}, @{text "..."} 
+  we can create files @{text "f\<^sub>1"}, @{text "f\<^sub>2"}, @{text "..."} 
   via @{text "CreateFile"}-events. This can be pictured roughly as follows:
 
   \begin{center}
@@ -785,23 +785,23 @@
   \begin{tabular}[t]{c}
   \\
   @{text "\<Longrightarrow>"}\\[2mm]
-  {\small@{term "CreateFile p (f\<^isub>1#pf)"}}
+  {\small@{term "CreateFile p (f\<^sub>1#pf)"}}
   \end{tabular}
   &
   \begin{tabular}[t]{c}
   \\
-  @{term "{p, pf, f\<^isub>1#pf}"}
+  @{term "{p, pf, f\<^sub>1#pf}"}
   \end{tabular} 
   &
   \begin{tabular}[t]{c}
   \\
   @{text "\<Longrightarrow>"}\\[2mm]
-  {\small@{term "CreateFile p (f\<^isub>2#f\<^isub>1#pf)"}}
+  {\small@{term "CreateFile p (f\<^sub>2#f\<^sub>1#pf)"}}
   \end{tabular}
   &
   \begin{tabular}[t]{c}
   \\
-  @{term "{p, pf, f\<^isub>1#pf, f\<^isub>2#f\<^isub>1#pf}"}
+  @{term "{p, pf, f\<^sub>1#pf, f\<^sub>2#f\<^sub>1#pf}"}
   \end{tabular} &
   \begin{tabular}[t]{c}
   \\
@@ -1035,34 +1035,34 @@
   is that there can be infinitely many valid states, but assuming the initial
   state contains only finitely many objects, then also @{term "all_sobjs"} will 
   be finite. To see the difference, consider the infinite ``chain'' of events 
-  just cloning a process @{text "p\<^isub>0"}:
+  just cloning a process @{text "p\<^sub>0"}:
 
   \begin{center}
   \begin{tabular}[t]{c@ {\hspace{-2mm}}c@ {\hspace{-2mm}}c@ {\hspace{-2mm}}c@ {\hspace{-2mm}}cc}
   \begin{tabular}[t]{c}
   Initial state:\\
-  @{term "{p\<^isub>0}"}
+  @{term "{p\<^sub>0}"}
   \end{tabular} &
   \begin{tabular}[t]{c}
   \\
   @{text "\<Longrightarrow>"}\\[2mm]
-  {\small@{term "Clone p\<^isub>0 p\<^isub>1"}}
+  {\small@{term "Clone p\<^sub>0 p\<^sub>1"}}
   \end{tabular}
   &
   \begin{tabular}[t]{c}
   \\
-  @{term "{p\<^isub>0, p\<^isub>1}"}
+  @{term "{p\<^sub>0, p\<^sub>1}"}
   \end{tabular} 
   &
   \begin{tabular}[t]{c}
   \\
   @{text "\<Longrightarrow>"}\\[2mm]
-  {\small@{term "Clone p\<^isub>0 p\<^isub>2"}}
+  {\small@{term "Clone p\<^sub>0 p\<^sub>2"}}
   \end{tabular}
   &
   \begin{tabular}[t]{c}
   \\
-  @{term "{p\<^isub>0, p\<^isub>1, p\<^isub>2}"}
+  @{term "{p\<^sub>0, p\<^sub>1, p\<^sub>2}"}
   \end{tabular} &
   \begin{tabular}[t]{c}
   \\
@@ -1077,22 +1077,22 @@
   \begin{center}
   \begin{tabular}[t]{cccc}
   \begin{tabular}[t]{c}
-  @{text "{P(r, dr, t, u)\<^bsup>Some (p\<^isub>0)\<^esup>}"}
+  @{text "{P(r, dr, t, u)\<^bsup>Some (p\<^sub>0)\<^esup>}"}
   \end{tabular} &
   \begin{tabular}[t]{c}
   @{text "\<Longrightarrow>"}
   \end{tabular}
   &
   \begin{tabular}[t]{c}
-  @{text "{P(r, dr, t, u)\<^bsup>Some (p\<^isub>0)\<^esup>, P(r, dr, t, u)\<^bsup>None\<^esup>}"}
+  @{text "{P(r, dr, t, u)\<^bsup>Some (p\<^sub>0)\<^esup>, P(r, dr, t, u)\<^bsup>None\<^esup>}"}
   \end{tabular} 
   \end{tabular}
   \end{center}
 
   \noindent
   where no further progress can be made because the information
-  recorded about @{text "p\<^isub>2"}, @{text "p\<^isub>3"} and so on is just the same
-  as for @{text "p\<^isub>1"}, namely @{text "P(r, dr, t, u)\<^bsup>None\<^esup>"}.  Indeed we
+  recorded about @{text "p\<^sub>2"}, @{text "p\<^sub>3"} and so on is just the same
+  as for @{text "p\<^sub>1"}, namely @{text "P(r, dr, t, u)\<^bsup>None\<^esup>"}.  Indeed we
   can prove the lemma:
 
   \begin{lemma}\label{finite}
@@ -1159,7 +1159,7 @@
   is that every tainted object is also reachable:
 
   \begin{lemma}
-  @{text "tainted\<^isup>s \<subseteq> reachable\<^isup>s"}
+  @{text "tainted\<^sup>s \<subseteq> reachable\<^sup>s"}
   \end{lemma}
 
   \noindent
@@ -1188,7 +1188,7 @@
 
   \begin{isabelle}\ \ \ \ \ %%%
   \mbox{\begin{tabular}{lcl}
-  @{thm (lhs) taintable_s_def} & @{text "\<equiv>"} & @{text "\<exists>item. item \<in> tainted\<^isup>s \<and> |item| = Some obj"}
+  @{thm (lhs) taintable_s_def} & @{text "\<equiv>"} & @{text "\<exists>item. item \<in> tainted\<^sup>s \<and> |item| = Some obj"}
   \end{tabular}}
   \end{isabelle}