diff -r 7fe2a20017c0 -r f9e0d3274c14 prio/Paper/Paper.thy --- a/prio/Paper/Paper.thy Mon Feb 27 18:53:53 2012 +0000 +++ b/prio/Paper/Paper.thy Tue Feb 28 13:13:32 2012 +0000 @@ -11,6 +11,7 @@ find_unused_assms PrioG find_unused_assms PrioGDef *) + ML {* open Printer; show_question_marks_default := false; @@ -1161,7 +1162,7 @@ \end{isabelle} \noindent - This means we do not need to add a holding edge to the @{text RAG} and no + This means we need to add a holding edge to the @{text RAG} and no current precedence needs to be recalculated.*}(*<*)end context step_P_cps_ne begin(*>*) text {* \noindent In the second case we know that resource @{text cs} is locked. We can show that