# HG changeset patch
# User paulson
# Date 842348123 -7200
# Node ID 30fe5ac5c04ee4ea0728f5332a18dfd041005c96
# Parent  2818289768e972db720f6c4049b795a9019812ce
Now runs all Auth proofs

diff -r 2818289768e9 -r 30fe5ac5c04e src/HOL/Auth/ROOT.ML
--- a/src/HOL/Auth/ROOT.ML	Tue Sep 10 11:07:49 1996 +0200
+++ b/src/HOL/Auth/ROOT.ML	Tue Sep 10 11:35:23 1996 +0200
@@ -3,7 +3,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 
-Root file for creating a separate database for protocol proofs.
+Root file for protocol proofs.
 *)
 
 HOL_build_completed;    (*Make examples fail if HOL did*)
@@ -11,13 +11,7 @@
 writeln"Root file for HOL/Auth";
 proof_timing := true;
 
-init_thy_reader();
+use_thy "Shared";
+use_thy "NS_Shared";
+use_thy "OtwayRees";
 
-(*Must be redefined in order to refer to the new instance of bind_thm
-  created by init_thy_reader.*)
-fun qed_spec_mp name =
-  let val thm = normalize_thm [RSspec,RSmp] (result())
-  in bind_thm(name, thm) end;
-
-use_thy "Shared";
-