--- 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"}