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 |