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