src/HOL/Auth/DB-ROOT.ML
author paulson
Fri Jul 04 17:34:55 1997 +0200 (1997-07-04)
changeset 3500 0d8ad2f192d8
parent 2563 e908e2716f3a
child 3511 da4dd8b7ced4
permissions -rw-r--r--
New constant "certificate"--just an abbreviation
paulson@1969
     1
(*  Title:      HOL/Auth/DB-ROOT
paulson@1969
     2
    ID:         $Id$
paulson@1969
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@1969
     4
    Copyright   1996  University of Cambridge
paulson@1969
     5
paulson@1969
     6
Root file for creating a **separate database** for protocol proofs.
paulson@1969
     7
             ** Use ROOT.ML to simply run the proofs. **
paulson@1969
     8
*)
paulson@1969
     9
paulson@1969
    10
HOL_build_completed;    (*Make examples fail if HOL did*)
paulson@1969
    11
paulson@1969
    12
val banner = "Security Protocols";
paulson@1969
    13
writeln banner;
paulson@1969
    14
paulson@1969
    15
init_thy_reader();
paulson@1969
    16
paulson@2326
    17
use_thy "Message";
paulson@1969
    18