| changeset 4449 | df30e75f670f |
| parent 4423 | a129b817b58a |
| child 4472 | cfa3bd184bc1 |
| 4448:b587d40ad474 | 4449:df30e75f670f |
|---|---|
17 rollback attacks). |
17 rollback attacks). |
18 *) |
18 *) |
19 |
19 |
20 open TLS; |
20 open TLS; |
21 |
21 |
22 proof_timing:=true; |
22 set proof_timing; |
23 HOL_quantifiers := false; |
23 HOL_quantifiers := false; |
24 |
24 |
25 (*Automatically unfold the definition of "certificate"*) |
25 (*Automatically unfold the definition of "certificate"*) |
26 Addsimps [certificate_def]; |
26 Addsimps [certificate_def]; |
27 |
27 |