| changeset 4449 | df30e75f670f |
| parent 4422 | 21238c9d363e |
| child 4471 | 0abf9d3f4391 |
| 4448:b587d40ad474 | 4449:df30e75f670f |
|---|---|
6 Inductive relation "recur" for the Recursive Authentication protocol. |
6 Inductive relation "recur" for the Recursive Authentication protocol. |
7 *) |
7 *) |
8 |
8 |
9 open Recur; |
9 open Recur; |
10 |
10 |
11 proof_timing:=true; |
11 set proof_timing; |
12 HOL_quantifiers := false; |
12 HOL_quantifiers := false; |
13 Pretty.setdepth 30; |
13 Pretty.setdepth 30; |
14 |
14 |
15 |
15 |
16 (** Possibility properties: traces that reach the end |
16 (** Possibility properties: traces that reach the end |