author | paulson |
Wed, 29 Jan 1997 15:34:23 +0100 | |
changeset 2563 | e908e2716f3a |
parent 2326 | 6df4488339e4 |
child 3511 | da4dd8b7ced4 |
permissions | -rw-r--r-- |
(* 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; init_thy_reader(); use_thy "Message";