| changeset 4449 | df30e75f670f |
| parent 4422 | 21238c9d363e |
| child 4470 | af3239def3d4 |
| 4448:b587d40ad474 | 4449:df30e75f670f |
|---|---|
12 Proc. Royal Soc. 426 (1989) |
12 Proc. Royal Soc. 426 (1989) |
13 *) |
13 *) |
14 |
14 |
15 open OtwayRees; |
15 open OtwayRees; |
16 |
16 |
17 proof_timing:=true; |
17 set proof_timing; |
18 HOL_quantifiers := false; |
18 HOL_quantifiers := false; |
19 |
19 |
20 |
20 |
21 (*A "possibility property": there are traces that reach the end*) |
21 (*A "possibility property": there are traces that reach the end*) |
22 goal thy |
22 goal thy |