--- 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";
-