author | wenzelm |
Sun, 15 Jul 2012 16:44:40 +0200 | |
changeset 48260 | 65ed3b2b3157 |
parent 48259 | 1635298d8fe7 |
child 48261 | 865610355ef3 |
--- 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}*}