# HG changeset patch
# User wenzelm
# Date 1342363480 -7200
# Node ID 65ed3b2b315757bccd1c4de7072a2531fe855250
# Parent  1635298d8fe7198c41a891b7b78a091c08547914
more precise imports;

diff -r 1635298d8fe7 -r 65ed3b2b3157 src/HOL/Auth/Guard/Guard_Public.thy
--- a/src/HOL/Auth/Guard/Guard_Public.thy	Sat Jul 14 21:15:41 2012 +0200
+++ b/src/HOL/Auth/Guard/Guard_Public.thy	Sun Jul 15 16:44:40 2012 +0200
@@ -5,7 +5,7 @@
 Lemmas on guarded messages for public protocols.
 *)
 
-theory Guard_Public imports Guard Public Extensions begin
+theory Guard_Public imports Guard "../Public" Extensions begin
 
 subsection{*Extensions to Theory @{text Public}*}