--- a/PIPBasics.thy	Thu Jan 28 13:46:45 2016 +0000
+++ b/PIPBasics.thy	Thu Jan 28 14:26:10 2016 +0000
@@ -2593,7 +2593,6 @@
 
 end
 
-
 lemma eq_RAG: 
   "RAG (wq s) = RAG s"
 by (unfold cs_RAG_def s_RAG_def, auto)