# HG changeset patch
# User paulson
# Date 849808988 -3600
# Node ID 6df4488339e4471ce992e003b7fb75f52a0d0a19
# Parent  ea8a1fc512e613c1c207a20c45f338cc2ef48819
Updating of banner

diff -r ea8a1fc512e6 -r 6df4488339e4 src/HOL/Auth/DB-ROOT.ML
--- a/src/HOL/Auth/DB-ROOT.ML	Thu Dec 05 19:01:49 1996 +0100
+++ b/src/HOL/Auth/DB-ROOT.ML	Thu Dec 05 19:03:08 1996 +0100
@@ -20,5 +20,5 @@
   let val thm = normalize_thm [RSspec,RSmp] (result())
   in bind_thm(name, thm) end;
 
-use_thy "Shared";
+use_thy "Message";