author | paulson |
Tue, 10 Sep 1996 11:35:23 +0200 | |
changeset 1971 | 30fe5ac5c04e |
parent 1944 | ea0f573b222b |
child 1995 | c80e58e78d9c |
permissions | -rw-r--r-- |
1944 | 1 |
(* Title: HOL/Auth/ROOT |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1996 University of Cambridge |
|
5 |
||
1971 | 6 |
Root file for protocol proofs. |
1944 | 7 |
*) |
8 |
||
9 |
HOL_build_completed; (*Make examples fail if HOL did*) |
|
10 |
||
11 |
writeln"Root file for HOL/Auth"; |
|
12 |
proof_timing := true; |
|
13 |
||
1971 | 14 |
use_thy "Shared"; |
15 |
use_thy "NS_Shared"; |
|
16 |
use_thy "OtwayRees"; |
|
1944 | 17 |