--- a/PrioG.thy	Sat May 24 12:39:12 2014 +0100
+++ b/PrioG.thy	Fri May 30 07:56:39 2014 +0100
@@ -994,7 +994,7 @@
       by (auto simp: s_RAG_def cs_waiting_def 
         cs_holding_def wq_def acyclic_def)
 qed
-qed
+
 
 lemma finite_RAG: 
   fixes s