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 |
|
|
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 |
|