Now runs all Auth proofs
authorpaulson
Tue Sep 10 11:35:23 1996 +0200 (1996-09-10)
changeset 197130fe5ac5c04e
parent 1970 2818289768e9
child 1972 cc65911dceef
Now runs all Auth proofs
src/HOL/Auth/ROOT.ML
     1.1 --- a/src/HOL/Auth/ROOT.ML	Tue Sep 10 11:07:49 1996 +0200
     1.2 +++ b/src/HOL/Auth/ROOT.ML	Tue Sep 10 11:35:23 1996 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1996  University of Cambridge
     1.6  
     1.7 -Root file for creating a separate database for protocol proofs.
     1.8 +Root file for protocol proofs.
     1.9  *)
    1.10  
    1.11  HOL_build_completed;    (*Make examples fail if HOL did*)
    1.12 @@ -11,13 +11,7 @@
    1.13  writeln"Root file for HOL/Auth";
    1.14  proof_timing := true;
    1.15  
    1.16 -init_thy_reader();
    1.17 +use_thy "Shared";
    1.18 +use_thy "NS_Shared";
    1.19 +use_thy "OtwayRees";
    1.20  
    1.21 -(*Must be redefined in order to refer to the new instance of bind_thm
    1.22 -  created by init_thy_reader.*)
    1.23 -fun qed_spec_mp name =
    1.24 -  let val thm = normalize_thm [RSspec,RSmp] (result())
    1.25 -  in bind_thm(name, thm) end;
    1.26 -
    1.27 -use_thy "Shared";
    1.28 -