# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1378468512 -3600
# Node ID dd1499f296ea23d77fc6468fbbeea019e63cee5b
# Parent  fb962189e9210a10a19eb589c14bce225575aca8
updated to new isabelle

diff -r fb962189e921 -r dd1499f296ea List_Prefix.thy
--- a/List_Prefix.thy	Sun Jun 23 03:55:49 2013 +0100
+++ b/List_Prefix.thy	Fri Sep 06 12:55:12 2013 +0100
@@ -119,7 +119,7 @@
   by (auto simp add: prefix_def)
 
 lemma prefix_same_cases:
-  "(xs\<^isub>1::'a list) \<le> ys \<Longrightarrow> xs\<^isub>2 \<le> ys \<Longrightarrow> xs\<^isub>1 \<le> xs\<^isub>2 \<or> xs\<^isub>2 \<le> xs\<^isub>1"
+  "(xs\<^sub>1::'a list) \<le> ys \<Longrightarrow> xs\<^sub>2 \<le> ys \<Longrightarrow> xs\<^sub>1 \<le> xs\<^sub>2 \<or> xs\<^sub>2 \<le> xs\<^sub>1"
   unfolding prefix_def by (metis append_eq_append_conv2)
 
 lemma set_mono_prefix: "xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys"
diff -r fb962189e921 -r dd1499f296ea Paper.thy
--- 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}
 
diff -r fb962189e921 -r dd1499f296ea document/isabelle.sty
--- a/document/isabelle.sty	Sun Jun 23 03:55:49 2013 +0100
+++ b/document/isabelle.sty	Fri Sep 06 12:55:12 2013 +0100
@@ -30,8 +30,6 @@
 \DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isaspacing\isastylescript##1}}}
 \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
-\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
-\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
 \DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isaspacing\isastylescript}
 \DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
 \DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isaspacing\isastylescript}
@@ -39,8 +37,6 @@
 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
 
 \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
-\newcommand{\isaantiqopen}{\isakeyword{\isacharbraceleft}}
-\newcommand{\isaantiqclose}{\isakeyword{\isacharbraceright}}
 
 \newdimen\isa@parindent\newdimen\isa@parskip
 
diff -r fb962189e921 -r dd1499f296ea document/isabellesym.sty
--- a/document/isabellesym.sty	Sun Jun 23 03:55:49 2013 +0100
+++ b/document/isabellesym.sty	Fri Sep 06 12:55:12 2013 +0100
@@ -322,13 +322,9 @@
 \newcommand{\isasymangle}{\isamath{\angle}}
 \newcommand{\isasymcopyright}{\isatext{\rm\copyright}}
 \newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
-\newcommand{\isasymhyphen}{\isatext{\rm-}}
 \newcommand{\isasyminverse}{\isamath{{}^{-1}}}
-\newcommand{\isasymonesuperior}{\isamath{{}^1}}
 \newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}}  %requires textcomp
-\newcommand{\isasymtwosuperior}{\isamath{{}^2}}
 \newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}}  %requires textcomp
-\newcommand{\isasymthreesuperior}{\isamath{{}^3}}
 \newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}}  %requires textcomp
 \newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
 \newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
@@ -342,6 +338,7 @@
 \newcommand{\isasymcent}{\isatext{\textcent}}  %requires textcomp
 \newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
 \newcommand{\isasymdegree}{\isatext{\rm\textdegree}}  %requires textcomp
+\newcommand{\isasymhyphen}{\isatext{\rm-}}
 \newcommand{\isasymamalg}{\isamath{\amalg}}
 \newcommand{\isasymmho}{\isamath{\mho}}  %requires amssymb
 \newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssymb