equal
deleted
inserted
replaced
497 |
497 |
498 \begin{isabelle}\ \ \ \ \ %%% |
498 \begin{isabelle}\ \ \ \ \ %%% |
499 \begin{tabular}{@ {}l} |
499 \begin{tabular}{@ {}l} |
500 @{thm (lhs) schs.simps(6)} @{text "\<equiv>"}\\ |
500 @{thm (lhs) schs.simps(6)} @{text "\<equiv>"}\\ |
501 \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\ |
501 \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\ |
502 \hspace{5mm}@{text "let"} @{text "new_wq = release (wq cs)"} @{text "in"}\\ |
502 \hspace{5mm}@{text "let"} @{text "new_wq = wq(cs := release (wq cs))"} @{text "in"}\\ |
503 \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|)"} |
503 \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|)"} |
504 \end{tabular} |
504 \end{tabular} |
505 \end{isabelle} |
505 \end{isabelle} |
506 |
506 |
507 Having the scheduler function @{term schs} at our disposal, we can ``lift'', or |
507 Having the scheduler function @{term schs} at our disposal, we can ``lift'', or |