--- a/prio/PrioGDef.thy	Mon Apr 23 08:01:37 2012 +0000
+++ b/prio/PrioGDef.thy	Mon Apr 30 15:32:34 2012 +0000
@@ -361,7 +361,15 @@
   @{text "th"} in state @{text "s"}.
   *}
 definition holdents :: "state \<Rightarrow> thread \<Rightarrow> cs set"
-  where "holdents s th \<equiv> {cs . (Cs cs, Th th) \<in> depend s}"
+  where "holdents s th \<equiv> {cs . holding s th cs}"
+
+lemma holdents_test: 
+  "holdents s th = {cs . (Cs cs, Th th) \<in> depend s}"
+unfolding holdents_def
+unfolding s_depend_def
+unfolding s_holding_abv
+unfolding wq_def
+by (simp)
 
 text {* \noindent
   @{text "cntCS s th"} returns the number of resources held by thread @{text "th"} in