--- a/CpsG.thy	Tue Jul 15 17:25:53 2014 +0200
+++ b/CpsG.thy	Wed Sep 09 11:24:19 2015 +0100
@@ -569,7 +569,7 @@
   from tranclD[OF this]
   obtain z where "(Th th, z) \<in> RAG s'" by auto
   with rd_th show "False"
-    apply (case_tac z, auto simp:readys_def s_waiting_def s_RAG_def s_waiting_def cs_waiting_def)
+    apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def)
     by (fold wq_def, blast)
 qed
 

--- a/Journal/Paper.thy	Tue Jul 15 17:25:53 2014 +0200
+++ b/Journal/Paper.thy	Wed Sep 09 11:24:19 2015 +0100
@@ -1157,9 +1157,9 @@
   a standard scheduling operation implemented in most operating
   systems.
 
-  \begin{proof}[of Lemma~\ref{childrenlem}]
-  Test
-  \end{proof}
+  %\begin{proof}[of Lemma~\ref{childrenlem}]
+  %Test
+  %\end{proof}
 
   Of course the main work for implementing PIP involves the
   scheduler and coding how it should react to events.  Below we

--- a/README	Tue Jul 15 17:25:53 2014 +0200
+++ b/README	Wed Sep 09 11:24:19 2015 +0100
@@ -12,7 +12,7 @@
 
 The repository can be checked using Isabelle 2013-2.
 
-  isabelle build -d . PIP
+  isabelle build -c -v -d . PIP
 
 
 Othe directories are:

--- a/ROOT	Tue Jul 15 17:25:53 2014 +0200
+++ b/ROOT	Wed Sep 09 11:24:19 2015 +0100
@@ -2,7 +2,7 @@
   theories [document = false]
 	"CpsG" 
 	"ExtGG"
-        (* "Test" *)
+        "Test" 
 
 session "Slides2" in "Slides" = PIP +
   options [document_variants="slides2"]

--- a/Test.thy	Tue Jul 15 17:25:53 2014 +0200
+++ b/Test.thy	Wed Sep 09 11:24:19 2015 +0100
@@ -749,10 +749,6 @@
 
 
 
-
-done
-
-
   (*
   obtain th0 where th0_in: "th0 \<in> S1 \<and> th0 \<in> S2" 
     and eq_f_th0: "preced th0 s = Max ((\<lambda>th. preced th s) ` (S1 \<inter> S2))"
@@ -784,4 +780,6 @@
   qed
   *)
 
+thm waits_def waits2_def
+
 end
\ No newline at end of file

Binary file journal.pdf has changed