equal
deleted
inserted
replaced
9 find_unused_assms Moment |
9 find_unused_assms Moment |
10 find_unused_assms Precedence_ord |
10 find_unused_assms Precedence_ord |
11 find_unused_assms PrioG |
11 find_unused_assms PrioG |
12 find_unused_assms PrioGDef |
12 find_unused_assms PrioGDef |
13 *) |
13 *) |
|
14 |
14 ML {* |
15 ML {* |
15 open Printer; |
16 open Printer; |
16 show_question_marks_default := false; |
17 show_question_marks_default := false; |
17 *} |
18 *} |
18 |
19 |
1159 @{thm eq_cp} |
1160 @{thm eq_cp} |
1160 \end{tabular} |
1161 \end{tabular} |
1161 \end{isabelle} |
1162 \end{isabelle} |
1162 |
1163 |
1163 \noindent |
1164 \noindent |
1164 This means we do not need to add a holding edge to the @{text RAG} and no |
1165 This means we need to add a holding edge to the @{text RAG} and no |
1165 current precedence needs to be recalculated.*}(*<*)end context step_P_cps_ne begin(*>*) text {* |
1166 current precedence needs to be recalculated.*}(*<*)end context step_P_cps_ne begin(*>*) text {* |
1166 \noindent |
1167 \noindent |
1167 In the second case we know that resource @{text cs} is locked. We can show that |
1168 In the second case we know that resource @{text cs} is locked. We can show that |
1168 |
1169 |
1169 \begin{isabelle}\ \ \ \ \ %%% |
1170 \begin{isabelle}\ \ \ \ \ %%% |