src/HOL/Auth/DB-ROOT.ML
author paulson
Thu, 05 Dec 1996 19:03:08 +0100
changeset 2326 6df4488339e4
parent 1969 af6d59e26dd9
child 2563 e908e2716f3a
permissions -rw-r--r--
Updating of banner
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
af6d59e26dd9 Dedicated root file for making the Auth database
paulson
parents:
diff changeset
    15
init_thy_reader();
af6d59e26dd9 Dedicated root file for making the Auth database
paulson
parents:
diff changeset
    16
af6d59e26dd9 Dedicated root file for making the Auth database
paulson
parents:
diff changeset
    17
(*Must be redefined in order to refer to the new instance of bind_thm
af6d59e26dd9 Dedicated root file for making the Auth database
paulson
parents:
diff changeset
    18
  created by init_thy_reader.*)
af6d59e26dd9 Dedicated root file for making the Auth database
paulson
parents:
diff changeset
    19
fun qed_spec_mp name =
af6d59e26dd9 Dedicated root file for making the Auth database
paulson
parents:
diff changeset
    20
  let val thm = normalize_thm [RSspec,RSmp] (result())
af6d59e26dd9 Dedicated root file for making the Auth database
paulson
parents:
diff changeset
    21
  in bind_thm(name, thm) end;
af6d59e26dd9 Dedicated root file for making the Auth database
paulson
parents:
diff changeset
    22
2326
6df4488339e4 Updating of banner
paulson
parents: 1969
diff changeset
    23
use_thy "Message";
1969
af6d59e26dd9 Dedicated root file for making the Auth database
paulson
parents:
diff changeset
    24