--- a/PrioGDef.thy	Sat Dec 22 01:58:45 2012 +0000
+++ b/PrioGDef.thy	Sat Dec 22 14:50:29 2012 +0000
@@ -169,6 +169,7 @@
   cs_dependents_def: 
   "dependents (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (depend wq)^+}"
 
+
 text {*
   The data structure used by the operating system for scheduling is referred to as 
   {\em schedule state}. It is represented as a record consisting of