equal
deleted
inserted
replaced
|
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 |
|
17 (*Must be redefined in order to refer to the new instance of bind_thm |
|
18 created by init_thy_reader.*) |
|
19 fun qed_spec_mp name = |
|
20 let val thm = normalize_thm [RSspec,RSmp] (result()) |
|
21 in bind_thm(name, thm) end; |
|
22 |
|
23 use_thy "Shared"; |
|
24 |