diff -r f1b39d77db00 -r ad57323fd4d6 PrioG.thy~
--- a/PrioG.thy~	Thu Dec 03 14:34:29 2015 +0800
+++ b/PrioG.thy~	Tue Dec 15 21:45:46 2015 +0800
@@ -210,7 +210,7 @@
     lemma \<lbrakk>thread \<in> set (wq_fun cs1 s); thread \<in> set (wq_fun cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2"
 *)
 
-text {* (* ??? *)
+text {* (* ddd *)
   The nature of the work is like this: since it starts from a very simple and basic 
   model, even intuitively very `basic` and `obvious` properties need to derived from scratch.
   For instance, the fact 
@@ -842,7 +842,7 @@
   qed
 qed
 
-text {* (* ??? *) 
+text {* (* ddd *) 
   The following @{text "step_RAG_v"} lemma charaterizes how @{text "RAG"} is changed
   with the happening of @{text "V"}-events:
 *}
@@ -1544,7 +1544,7 @@
   ultimately show ?thesis by (simp add:cntCS_def)
 qed 
 
-text {* (* ??? *) \noindent
+text {* (* ddd *) \noindent
   The relationship between @{text "cntP"}, @{text "cntV"} and @{text "cntCS"} 
   of one particular thread. 
 *}