--- a/Implementation.thy	Thu Jun 29 14:59:55 2017 +0100
+++ b/Implementation.thy	Thu Jun 29 15:31:24 2017 +0100
@@ -70,7 +70,7 @@
 *}
 
 lemma cp_rec_tG:
-  "cp s th = Max (preceds {th} s \<union> cprecs (children (tG s) th) s)"
+  "cp s th = Max ({preced th s} \<union> cprecs (children (tG s) th) s)"
 proof -
   have [simp]: "(cp s \<circ> the_thread \<circ> Th) = cp s" by (rule ext, simp)
   have [simp]: "(cp s \<circ> the_thread) ` children (tRAG s) (Th th) =