26 |
26 |
27 |
27 |
28 declare [[show_question_marks = false]] |
28 declare [[show_question_marks = false]] |
29 |
29 |
30 notation (latex output) |
30 notation (latex output) |
31 Cons ("_::_" [78,77] 73) and |
31 Cons ("_::_" [78,77] 73) |
32 If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and |
32 |
|
33 notation (latex output) |
33 vt ("valid'_state") and |
34 vt ("valid'_state") and |
34 Prc ("'(_, _')") and |
35 Prc ("'(_, _')") and |
35 holding_raw ("holds") and |
36 holding_raw ("holds") and |
36 holding ("holds") and |
37 holding ("holds") and |
37 waiting_raw ("waits") and |
38 waiting_raw ("waits") |
|
39 |
|
40 notation (latex output) |
38 waiting ("waits") and |
41 waiting ("waits") and |
39 tG_raw ("TDG") and |
42 tG_raw ("TDG") and |
40 tG ("TDG") and |
43 tG ("TDG") and |
41 RAG_raw ("RAG") and |
44 RAG_raw ("RAG") and |
42 RAG ("RAG") and |
45 RAG ("RAG") and |
43 Th ("T") and |
46 Th ("T") |
|
47 |
|
48 notation (latex output) |
44 Cs ("C") and |
49 Cs ("C") and |
45 readys ("ready") and |
50 readys ("ready") and |
46 preced ("prec") and |
51 preced ("prec") and |
47 preceds ("precs") and |
52 preceds ("precs") and |
48 cpreced ("cprec") and |
53 cpreced ("cprec") and |
49 cpreceds ("cprecs") and |
54 cpreceds ("cprecs") and |
50 (*wq_fun ("wq") and*) |
|
51 cp ("cprec") and |
55 cp ("cprec") and |
52 (*cprec_fun ("cp_fun") and*) |
56 holdents ("resources") and |
53 holdents ("resources") and |
|
54 DUMMY ("\<^raw:\mbox{$\_\!\_$}>") and |
|
55 cntP ("c\<^bsub>P\<^esub>") and |
57 cntP ("c\<^bsub>P\<^esub>") and |
56 cntV ("c\<^bsub>V\<^esub>") |
58 cntV ("c\<^bsub>V\<^esub>") |
57 |
59 |
58 |
60 notation (latex output) |
|
61 DUMMY ("\<^latex>\<open>\\mbox{$\\_\\!\\_$}\<close>") |
|
62 |
|
63 notation (latex output) |
|
64 If ("(\<^latex>\<open>\\textrm{\<close>if\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>then\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>else\<^latex>\<open>}\<close> (_))" 10) |
59 (*>*) |
65 (*>*) |
60 |
66 |
61 section {* Introduction *} |
67 section {* Introduction *} |
62 |
68 |
63 text {* |
69 text {* |