Moving common declarations and proofs from theories "Shared"
and "Public" to "Event". NB the original "Event" theory was later renamed "Shared".
Addition of the Notes constructor to datatype "event".
(* Title: HOL/Auth/DB-ROOT
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
Root file for creating a **separate database** for protocol proofs.
** Use ROOT.ML to simply run the proofs. **
*)
HOL_build_completed; (*Make examples fail if HOL did*)
val banner = "Security Protocols";
writeln banner;
use_thy "Message";