changeset 5492 | d9fc3457554e |
parent 5491 | 22f8331cdf47 |
child 5493 | e335c51808ac |
5491:22f8331cdf47 | 5492:d9fc3457554e |
---|---|
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 use_thy "Event"; |