--- a/PrioGDef.thy	Tue May 20 12:49:21 2014 +0100
+++ b/PrioGDef.thy	Thu May 22 17:40:39 2014 +0100
@@ -121,7 +121,7 @@
 consts 
   holding :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool" 
   waiting :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool"
-  depend :: "'b \<Rightarrow> (node \<times> node) set"
+  RAG :: "'b \<Rightarrow> (node \<times> node) set"
   dependants :: "'b \<Rightarrow> thread \<Rightarrow> thread set"
 
 text {*
@@ -153,21 +153,21 @@
   "waiting wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread \<noteq> hd (wq cs))"
   -- {* 
   \begin{minipage}{0.9\textwidth}
-  @{text "depend wq"} represents the Resource Allocation Graph of the system under the waiting 
+  @{text "RAG wq"} represents the Resource Allocation Graph of the system under the waiting 
   queue function @{text "wq"}.
   \end{minipage}
   *}
-  cs_depend_def: 
-  "depend (wq::cs \<Rightarrow> thread list) \<equiv>
+  cs_RAG_def: 
+  "RAG (wq::cs \<Rightarrow> thread list) \<equiv>
       {(Th th, Cs cs) | th cs. waiting wq th cs} \<union> {(Cs cs, Th th) | cs th. holding wq th cs}"
   -- {* 
   \begin{minipage}{0.9\textwidth}
-  The following @{text "dependants wq th"} represents the set of threads which are depending on
-  thread @{text "th"} in Resource Allocation Graph @{text "depend wq"}:
+  The following @{text "dependants wq th"} represents the set of threads which are RAGing on
+  thread @{text "th"} in Resource Allocation Graph @{text "RAG wq"}:
   \end{minipage}
   *}
   cs_dependants_def: 
-  "dependants (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (depend wq)^+}"
+  "dependants (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (RAG wq)^+}"
 
 
 text {*
@@ -243,7 +243,7 @@
       \item For other happening event, the schedule state just does not change.
   \end{enumerate}
   \item @{text "ncp"} is new precedence function, it is calculated from the newly updated waiting queue 
-        function. The dependency of precedence function on waiting queue function is the reason to 
+        function. The RAGency of precedence function on waiting queue function is the reason to 
         put them in the same record so that they can evolve together.
   \end{enumerate}
   \end{minipage}
@@ -269,7 +269,7 @@
 lemma cpreced_initial: 
   "cpreced (\<lambda> cs. []) [] = (\<lambda>_. (Prc 0 0))"
 apply(simp add: cpreced_def)
-apply(simp add: cs_dependants_def cs_depend_def cs_waiting_def cs_holding_def)
+apply(simp add: cs_dependants_def cs_RAG_def cs_waiting_def cs_holding_def)
 apply(simp add: preced_def)
 done
 
@@ -305,9 +305,9 @@
   where "cp s \<equiv> cprec_fun (schs s)"
 
 text {* \noindent
-  Functions @{text "holding"}, @{text "waiting"}, @{text "depend"} and 
+  Functions @{text "holding"}, @{text "waiting"}, @{text "RAG"} and 
   @{text "dependants"} still have the 
-  same meaning, but redefined so that they no longer depend on the 
+  same meaning, but redefined so that they no longer RAG on the 
   fictitious {\em waiting queue function}
   @{text "wq"}, but on system state @{text "s"}.
   *}
@@ -316,8 +316,8 @@
   "holding (s::state) \<equiv> holding (wq_fun (schs s))"
   s_waiting_abv: 
   "waiting (s::state) \<equiv> waiting (wq_fun (schs s))"
-  s_depend_abv: 
-  "depend (s::state) \<equiv> depend (wq_fun (schs s))"
+  s_RAG_abv: 
+  "RAG (s::state) \<equiv> RAG (wq_fun (schs s))"
   s_dependants_abv: 
   "dependants (s::state) \<equiv> dependants (wq_fun (schs s))"
 
@@ -334,14 +334,14 @@
   "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: 
-  "depend (s::state) =
+lemma s_RAG_def: 
+  "RAG (s::state) =
     {(Th th, Cs cs) | th cs. waiting (wq s) th cs} \<union> {(Cs cs, Th th) | cs th. holding (wq s) th cs}"
-  by (auto simp:s_depend_abv wq_def cs_depend_def)
+  by (auto simp:s_RAG_abv wq_def cs_RAG_def)
 
 lemma
   s_dependants_def: 
-  "dependants (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (depend (wq s))^+}"
+  "dependants (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (RAG (wq s))^+}"
   by (auto simp:s_dependants_abv wq_def cs_dependants_def)
 
 text {*
@@ -366,9 +366,9 @@
   where "holdents s th \<equiv> {cs . holding s th cs}"
 
 lemma holdents_test: 
-  "holdents s th = {cs . (Cs cs, Th th) \<in> depend s}"
+  "holdents s th = {cs . (Cs cs, Th th) \<in> RAG s}"
 unfolding holdents_def
-unfolding s_depend_def
+unfolding s_RAG_def
 unfolding s_holding_abv
 unfolding wq_def
 by (simp)
@@ -403,7 +403,7 @@
   carefully programmed so that deadlock can not happen:
   \end{minipage}
   *}
-  thread_P: "\<lbrakk>thread \<in> runing s;  (Cs cs, Th thread)  \<notin> (depend s)^+\<rbrakk> \<Longrightarrow> 
+  thread_P: "\<lbrakk>thread \<in> runing s;  (Cs cs, Th thread)  \<notin> (RAG s)^+\<rbrakk> \<Longrightarrow> 
                                                                 step s (P thread cs)" |
   -- {*
   \begin{minipage}{0.9\textwidth}