# HG changeset patch
# User paulson
# Date 841768215 -7200
# Node ID ea0f573b222b73eead61e1272534ed3ef9b16434
# Parent  20574dca5a3eb3c0b7191c0235403e35cb1ad40d
ROOT file for Auth directory

diff -r 20574dca5a3e -r ea0f573b222b src/HOL/Auth/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/ROOT.ML	Tue Sep 03 18:30:15 1996 +0200
@@ -0,0 +1,23 @@
+(*  Title:      HOL/Auth/ROOT
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1996  University of Cambridge
+
+Root file for creating a separate database for protocol proofs.
+*)
+
+HOL_build_completed;    (*Make examples fail if HOL did*)
+
+writeln"Root file for HOL/Auth";
+proof_timing := true;
+
+init_thy_reader();
+
+(*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";
+