diff -r dd1499f296ea -r d43f46423298 Paper.thy
--- a/Paper.thy	Fri Sep 06 12:55:12 2013 +0100
+++ b/Paper.thy	Fri Sep 06 13:27:46 2013 +0100
@@ -534,7 +534,7 @@
   \noindent
   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 ``randomly'' generated by the operating system, but this process ID should
+  ID generated by the operating system, but this process ID should
   not already exist. The admissibility rules for the other events impose similar conditions. 
 
   However, the admissibility check by the operating system is only one