--- a/Paper.thy	Thu Jun 13 22:53:49 2013 +0800
+++ b/Paper.thy	Sun Jun 16 20:42:07 2013 -0400
@@ -300,8 +300,8 @@
   model of the operating system.  With these two results in place we
   can show that a static policy check is sufficient in order to
   guarantee the access properties before running the system. Again as
-  far as we know, no such check that is the operating
-  system behaviour has been designed before.
+  far as we know, no such check has been designed and proved correct 
+  before.
   
 
   %Specified dynamic behaviour of the system; 
@@ -535,10 +535,10 @@
   Clearly the operating system should only allow to clone a process @{text p} if the 
   process is currently alive. The cloned process will get the process
   ID generated by the function @{term new_proc}. This process ID should
-  not already exist. Therefore we define @{term new_proc} as
+  not already exist. Therefore we define @{term new_proc} as *}
 
   (* HERE ????? chunhan *)
-
+text {*
   \begin{isabelle}\ \ \ \ \ %%%
   \mbox{\begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
   @{term "new_proc s"} & @{text "\<equiv>"} & @{term "Max (current_procs s) + 1"}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ROOT	Sun Jun 16 20:42:07 2013 -0400
@@ -0,0 +1,13 @@
+session "RC" = HOL +
+  theories [document = false]
+	"rc_theory" 
+	"final_theorems" 
+	"rc_theory" 
+	"os_rc" 
+
+session "Paper" = RC +
+  options [document = pdf, browser_info = false, document_output = "."]
+  theories
+    "Paper"
+
+

--- a/document/isabelle.sty	Thu Jun 13 22:53:49 2013 +0800
+++ b/document/isabelle.sty	Sun Jun 16 20:42:07 2013 -0400
@@ -103,9 +103,6 @@
 \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
 }
 
-\newcommand{\isaliteral}[2]{#2}
-\newcommand{\isanil}{}
-
 
 % keyword and section markup
 
@@ -158,9 +155,9 @@
 \isachardefaults%
 \def\isacharunderscorekeyword{\mbox{-}}%
 \def\isacharbang{\isamath{!}}%
-\def\isachardoublequote{\isanil}%
-\def\isachardoublequoteopen{\isanil}%
-\def\isachardoublequoteclose{\isanil}%
+\def\isachardoublequote{}%
+\def\isachardoublequoteopen{}%
+\def\isachardoublequoteclose{}%
 \def\isacharhash{\isamath{\#}}%
 \def\isachardollar{\isamath{\$}}%
 \def\isacharpercent{\isamath{\%}}%

--- a/document/root.tex	Thu Jun 13 22:53:49 2013 +0800
+++ b/document/root.tex	Sun Jun 16 20:42:07 2013 -0400
@@ -56,21 +56,21 @@
 %%\mprset{center=false}
 \mprset{flushleft}
 \begin{document}
-\pagestyle{empty}
+%\pagestyle{empty}
 
-\noindent
-The co-authors Xingyuan Zhang and Christian Urban attest that the student 
-Chunhan Wu did all the central
-work concerning the paper.\bigskip\bigskip
+%\noindent
+%The co-authors Xingyuan Zhang and Christian Urban attest that the student 
+%Chunhan Wu did all the central
+%work concerning the paper.\bigskip\bigskip
 
-\includegraphics[scale=0.9]{xingyuan.jpg}\\
-\noindent
-Xingyuan Zhang
-\bigskip\bigskip
+%\includegraphics[scale=0.9]{xingyuan.jpg}\\
+%\noindent
+%Xingyuan Zhang
+%\bigskip\bigskip
 
-\mbox{}\hspace{-8mm}\includegraphics[scale=1.2]{christian.jpg}\\
-\noindent
-Christian Urban
+%\mbox{}\hspace{-8mm}\includegraphics[scale=1.2]{christian.jpg}\\
+%\noindent
+%Christian Urban
 
 
 \newpage

Binary file paper.pdf has changed