--- a/prio/Paper/Paper.thy	Sat Feb 11 09:14:14 2012 +0000
+++ b/prio/Paper/Paper.thy	Sat Feb 11 09:34:46 2012 +0000
@@ -23,8 +23,6 @@
   preced ("prec") and
   cpreced ("cprec") and
   dependents ("dependants") and
-  waiting_queue ("wq_fun") and
-  cur_preced ("cprec_fun") and
   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")
 (*>*)
 
@@ -362,13 +360,16 @@
   @{text "\<lparr>wq_fun, cprec_fun\<rparr>"}
   \end{isabelle}
 
+  \noindent
+  We have the usual getter and setter methods for such records.
+
   In the initial state, the scheduler starts with all resources unlocked and the
   precedence of every thread is initialised with @{term "Prc 0 0"}. 
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
   @{thm (lhs) schs.simps(1)} @{text "\<equiv>"}\\ 
-  \hspace{5mm}@{term "(|waiting_queue = all_unlocked, cur_preced = (\<lambda>_::thread. Prc 0 0)|)"}
+  \hspace{5mm}@{term "(|wq_fun = all_unlocked, cprec_fun = (\<lambda>_::thread. Prc 0 0)|)"}
   \end{tabular}
   \end{isabelle}
 
@@ -382,14 +383,14 @@
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
   @{thm (lhs) schs.simps(2)} @{text "\<equiv>"}\\ 
-  \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\
-  \hspace{8mm}@{term "(|waiting_queue = wq\<iota>, cur_preced = cpreced wq\<iota> (Create th prio # s)|)"}\\
+  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
+  \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Create th prio # s)|)"}\\
   @{thm (lhs) schs.simps(3)} @{text "\<equiv>"}\\
-  \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\
-  \hspace{8mm}@{term "(|waiting_queue = wq\<iota>, cur_preced = cpreced wq\<iota> (Exit th # s)|)"}\smallskip\\
+  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
+  \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Exit th # s)|)"}\smallskip\\
   @{thm (lhs) schs.simps(4)} @{text "\<equiv>"}\\ 
-  \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\
-  \hspace{8mm}@{term "(|waiting_queue = wq\<iota>, cur_preced = cpreced wq\<iota> (Set th prio # s)|)"}
+  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
+  \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Set th prio # s)|)"}
   \end{tabular}
   \end{isabelle}
 
@@ -403,9 +404,9 @@
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
   @{thm (lhs) schs.simps(5)} @{text "\<equiv>"}\\ 
-  \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\
+  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
   \hspace{5mm}@{text "let"} @{text "new_wq = wq(cs := (wq cs @ [th]))"} @{text "in"}\\
-  \hspace{8mm}@{term "(|waiting_queue = new_wq, cur_preced = cpreced new_wq (P th cs # s)|)"}
+  \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|)"}
   \end{tabular}
   \end{isabelle}
 
@@ -423,9 +424,9 @@
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
   @{thm (lhs) schs.simps(6)} @{text "\<equiv>"}\\
-  \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\
+  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
   \hspace{5mm}@{text "let"} @{text "new_wq = release (wq cs)"} @{text "in"}\\
-  \hspace{8mm}@{term "(|waiting_queue = new_wq, cur_preced = cpreced new_wq (V th cs # s)|)"}
+  \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|)"}
   \end{tabular}
   \end{isabelle}