ROOT file for Auth directory
authorpaulson
Tue Sep 03 18:30:15 1996 +0200 (1996-09-03)
changeset 1944ea0f573b222b
parent 1943 20574dca5a3e
child 1945 20ca9cf90e69
ROOT file for Auth directory
src/HOL/Auth/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Auth/ROOT.ML	Tue Sep 03 18:30:15 1996 +0200
     1.3 @@ -0,0 +1,23 @@
     1.4 +(*  Title:      HOL/Auth/ROOT
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1996  University of Cambridge
     1.8 +
     1.9 +Root file for creating a separate database for protocol proofs.
    1.10 +*)
    1.11 +
    1.12 +HOL_build_completed;    (*Make examples fail if HOL did*)
    1.13 +
    1.14 +writeln"Root file for HOL/Auth";
    1.15 +proof_timing := true;
    1.16 +
    1.17 +init_thy_reader();
    1.18 +
    1.19 +(*Must be redefined in order to refer to the new instance of bind_thm
    1.20 +  created by init_thy_reader.*)
    1.21 +fun qed_spec_mp name =
    1.22 +  let val thm = normalize_thm [RSspec,RSmp] (result())
    1.23 +  in bind_thm(name, thm) end;
    1.24 +
    1.25 +use_thy "Shared";
    1.26 +