diff -r 313acffe63b6 -r 92f61f6a0fe7 ExtGG.thy --- a/ExtGG.thy Tue May 20 12:49:21 2014 +0100 +++ b/ExtGG.thy Thu May 22 17:40:39 2014 +0100 @@ -978,7 +978,7 @@ from th_kept have "th \ threads (t@s)" by auto from th_chain_to_ready[OF vt_t this] and not_ready obtain th' where th'_in: "th' \ readys (t@s)" - and dp: "(Th th, Th th') \ (depend (t @ s))\<^sup>+" by auto + and dp: "(Th th, Th th') \ (RAG (t @ s))\<^sup>+" by auto have "th' \ runing (t@s)" proof - have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" @@ -1021,7 +1021,7 @@ next from dp have "th \ dependants (wq (t @ s)) th'" - by (unfold cs_dependants_def, auto simp:eq_depend) + by (unfold cs_dependants_def, auto simp:eq_RAG) thus "preced th (t @ s) \ (\th. preced th (t @ s)) ` ({th'} \ dependants (wq (t @ s)) th')" by auto