author | paulson |
Wed, 29 Jan 1997 15:34:23 +0100 | |
changeset 2563 | e908e2716f3a |
parent 2326 | 6df4488339e4 |
child 3511 | da4dd8b7ced4 |
permissions | -rw-r--r-- |
1969 | 1 |
(* Title: HOL/Auth/DB-ROOT |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1996 University of Cambridge |
|
5 |
||
6 |
Root file for creating a **separate database** for protocol proofs. |
|
7 |
** Use ROOT.ML to simply run the proofs. ** |
|
8 |
*) |
|
9 |
||
10 |
HOL_build_completed; (*Make examples fail if HOL did*) |
|
11 |
||
12 |
val banner = "Security Protocols"; |
|
13 |
writeln banner; |
|
14 |
||
15 |
init_thy_reader(); |
|
16 |
||
2326 | 17 |
use_thy "Message"; |
1969 | 18 |