| changeset 9000 | c20d58286a51 |
| parent 7239 | 26685edee372 |
| child 13508 | 890d736b93a5 |
| 8999:ad8260dc6e4a | 9000:c20d58286a51 |
|---|---|
4 Copyright 1996 University of Cambridge |
4 Copyright 1996 University of Cambridge |
5 |
5 |
6 Root file for protocol proofs. |
6 Root file for protocol proofs. |
7 *) |
7 *) |
8 |
8 |
9 writeln"Root file for HOL/Auth"; |
|
10 |
|
11 set proof_timing; |
|
12 goals_limit := 1; |
9 goals_limit := 1; |
13 |
10 |
14 (*Shared-key protocols*) |
11 (*Shared-key protocols*) |
15 time_use_thy "NS_Shared"; |
12 time_use_thy "NS_Shared"; |
16 time_use_thy "Kerberos_BAN"; |
13 time_use_thy "Kerberos_BAN"; |