equal
deleted
inserted
replaced
13 |
13 |
14 text{*From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.*} |
14 text{*From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.*} |
15 |
15 |
16 subsection{*Definitions*} |
16 subsection{*Definitions*} |
17 |
17 |
18 datatype_new pstate = Hungry | Eating | Thinking |
18 datatype pstate = Hungry | Eating | Thinking |
19 --{*process states*} |
19 --{*process states*} |
20 |
20 |
21 record state = |
21 record state = |
22 token :: "nat" |
22 token :: "nat" |
23 proc :: "nat => pstate" |
23 proc :: "nat => pstate" |