--- a/prio/PrioGDef.thy	Sat Feb 11 19:39:50 2012 +0000
+++ b/prio/PrioGDef.thy	Sun Feb 12 04:45:20 2012 +0000
@@ -300,7 +300,7 @@
   The following @{text "cp"} is a shorthand for @{text "cprec_fun"}. 
   *}
 definition cp :: "state \<Rightarrow> thread \<Rightarrow> precedence"
-  where "cp s = cprec_fun (schs s)"
+  where "cp s \<equiv> cprec_fun (schs s)"
 
 text {* \noindent
   Functions @{text "holding"}, @{text "waiting"}, @{text "depend"} and 
@@ -311,13 +311,13 @@
   *}
 defs (overloaded) 
   s_holding_abv: 
-  "holding (s::state) \<equiv> holding (wq s)"
+  "holding (s::state) \<equiv> holding (wq_fun (schs s))"
   s_waiting_abv: 
-  "waiting (s::state) \<equiv> waiting (wq s)"
+  "waiting (s::state) \<equiv> waiting (wq_fun (schs s))"
   s_depend_abv: 
-  "depend (s::state) \<equiv> depend (wq s)"
+  "depend (s::state) \<equiv> depend (wq_fun (schs s))"
   s_dependents_abv: 
-  "dependents (s::state) th \<equiv> dependents (wq s) th"
+  "dependents (s::state) \<equiv> dependents (wq_fun (schs s))"
 
 
 text {* 
@@ -325,11 +325,11 @@
   *}
 lemma
   s_holding_def: 
-  "holding (s::state) thread cs = (thread \<in> set (wq s cs) \<and> thread = hd (wq s cs))"
+  "holding (s::state) th cs \<equiv> (th \<in> set (wq_fun (schs s) cs) \<and> th = hd (wq_fun (schs s) cs))"
   by (auto simp:s_holding_abv wq_def cs_holding_def)
 
 lemma s_waiting_def: 
-  "waiting (s::state) thread cs = (thread \<in> set (wq s cs) \<and> thread \<noteq> hd (wq s cs))"
+  "waiting (s::state) th cs \<equiv> (th \<in> set (wq_fun (schs s) cs) \<and> th \<noteq> hd (wq_fun (schs s) cs))"
   by (auto simp:s_waiting_abv wq_def cs_waiting_def)
 
 lemma s_depend_def: 
@@ -354,14 +354,14 @@
   thread with the highest precedence. 
   *}
 definition runing :: "state \<Rightarrow> thread set"
-  where "runing s = {th . th \<in> readys s \<and> cp s th = Max ((cp s) ` (readys s))}"
+  where "runing s \<equiv> {th . th \<in> readys s \<and> cp s th = Max ((cp s) ` (readys s))}"
 
 text {* \noindent
   The following function @{text "holdents s th"} returns the set of resources held by thread 
   @{text "th"} in state @{text "s"}.
   *}
 definition holdents :: "state \<Rightarrow> thread \<Rightarrow> cs set"
-  where "holdents s th = {cs . (Cs cs, Th th) \<in> depend s}"
+  where "holdents s th \<equiv> {cs . (Cs cs, Th th) \<in> depend s}"
 
 text {* \noindent
   @{text "cntCS s th"} returns the number of resources held by thread @{text "th"} in
@@ -412,18 +412,17 @@
   Priority Inheritance protocol can be expressed as: @{text "vt step s"}, where
   the predicate @{text "vt"} can be defined as the following:
   *}
-inductive vt :: "(state \<Rightarrow> event \<Rightarrow> bool) \<Rightarrow> state \<Rightarrow> bool"
- for cs -- {* @{text "cs"} is an argument representing any step predicate. *}
+inductive vt :: "state \<Rightarrow> bool"
   where
   -- {* Empty list @{text "[]"} is a legal state in any protocol:*}
-  vt_nil[intro]: "vt cs []" |
+  vt_nil[intro]: "vt []" |
   -- {* 
   \begin{minipage}{0.9\textwidth}
   If @{text "s"} a legal state, and event @{text "e"} is eligible to happen
   in state @{text "s"}, then @{text "e#s"} is a legal state as well:
   \end{minipage}
   *}
-  vt_cons[intro]: "\<lbrakk>vt cs s; cs s e\<rbrakk> \<Longrightarrow> vt cs (e#s)"
+  vt_cons[intro]: "\<lbrakk>vt s; step s e\<rbrakk> \<Longrightarrow> vt (e#s)"
 
 text {*  \noindent
   It is easy to see that the definition of @{text "vt"} is generic. It can be applied to