| changeset 4449 | df30e75f670f |
| parent 4422 | 21238c9d363e |
| child 4471 | 0abf9d3f4391 |
| 4448:b587d40ad474 | 4449:df30e75f670f |
|---|---|
10 Proc. Royal Soc. 426 (1989) |
10 Proc. Royal Soc. 426 (1989) |
11 *) |
11 *) |
12 |
12 |
13 open Yahalom; |
13 open Yahalom; |
14 |
14 |
15 proof_timing:=true; |
15 set proof_timing; |
16 HOL_quantifiers := false; |
16 HOL_quantifiers := false; |
17 Pretty.setdepth 25; |
17 Pretty.setdepth 25; |
18 |
18 |
19 |
19 |
20 (*A "possibility property": there are traces that reach the end*) |
20 (*A "possibility property": there are traces that reach the end*) |