src/HOL/Auth/DB-ROOT.ML
author paulson
Fri, 11 Jul 1997 13:26:15 +0200
changeset 3512 9dcb4daa15e8
parent 3511 da4dd8b7ced4
child 3513 4d4f8c18255e
permissions -rw-r--r--
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".
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1969
af6d59e26dd9 Dedicated root file for making the Auth database
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/DB-ROOT
af6d59e26dd9 Dedicated root file for making the Auth database
paulson
parents:
diff changeset
     2
    ID:         $Id$
af6d59e26dd9 Dedicated root file for making the Auth database
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
af6d59e26dd9 Dedicated root file for making the Auth database
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
af6d59e26dd9 Dedicated root file for making the Auth database
paulson
parents:
diff changeset
     5
af6d59e26dd9 Dedicated root file for making the Auth database
paulson
parents:
diff changeset
     6
Root file for creating a **separate database** for protocol proofs.
af6d59e26dd9 Dedicated root file for making the Auth database
paulson
parents:
diff changeset
     7
             ** Use ROOT.ML to simply run the proofs. **
af6d59e26dd9 Dedicated root file for making the Auth database
paulson
parents:
diff changeset
     8
*)
af6d59e26dd9 Dedicated root file for making the Auth database
paulson
parents:
diff changeset
     9
af6d59e26dd9 Dedicated root file for making the Auth database
paulson
parents:
diff changeset
    10
HOL_build_completed;    (*Make examples fail if HOL did*)
af6d59e26dd9 Dedicated root file for making the Auth database
paulson
parents:
diff changeset
    11
af6d59e26dd9 Dedicated root file for making the Auth database
paulson
parents:
diff changeset
    12
val banner = "Security Protocols";
af6d59e26dd9 Dedicated root file for making the Auth database
paulson
parents:
diff changeset
    13
writeln banner;
af6d59e26dd9 Dedicated root file for making the Auth database
paulson
parents:
diff changeset
    14
2326
6df4488339e4 Updating of banner
paulson
parents: 1969
diff changeset
    15
use_thy "Message";