src/HOL/Auth/DB-ROOT.ML
author paulson
Thu Jan 08 18:10:34 1998 +0100 (1998-01-08)
changeset 4537 4e835bd9fada
parent 3513 4d4f8c18255e
permissions -rw-r--r--
Expressed most Oops rules using Notes instead of Says, and other tidying
     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";