Changing "lost" from a parameter of protocol definitions to a constant.
Advantages: no "lost" argument everywhere; fewer Vars in subgoals;
less need for specially instantiated rules
Disadvantage: can no longer prove "Agent_not_see_encrypted_key", but this
theorem was never used, and its original proof was also broken
the introduction of the "Notes" constructor.
(* 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 "Event";