--- a/PIPBasics.thy~	Thu Jan 28 13:46:45 2016 +0000
+++ b/PIPBasics.thy~	Thu Jan 28 14:26:10 2016 +0000
@@ -3786,6 +3786,7 @@
 
 end
 
+
 -- {* A useless definition *}
 definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"
 where "cps s = {(th, cp s th) | th . th \<in> threads s}"