| changeset 2378 | fc103154ad8f |
| parent 2284 | 80ebd1a213fd |
| child 2451 | ce85a2aafc7a |
| 2377:ad9d2dedaeaa | 2378:fc103154ad8f |
|---|---|
12 Proc. Royal Soc. 426 (1989) |
12 Proc. Royal Soc. 426 (1989) |
13 *) |
13 *) |
14 |
14 |
15 OtwayRees = Shared + |
15 OtwayRees = Shared + |
16 |
16 |
17 consts otway :: "agent set => event list set" |
17 consts otway :: agent set => event list set |
18 inductive "otway lost" |
18 inductive "otway lost" |
19 intrs |
19 intrs |
20 (*Initial trace is empty*) |
20 (*Initial trace is empty*) |
21 Nil "[]: otway lost" |
21 Nil "[]: otway lost" |
22 |
22 |