| changeset 16417 | 9bc16273c2d4 |
| parent 13508 | 890d736b93a5 |
| child 20768 | 1d478c2d621f |
--- a/src/HOL/Auth/Guard/List_Msg.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/Auth/Guard/List_Msg.thy Fri Jun 17 16:12:49 2005 +0200 @@ -11,7 +11,7 @@ header{*Lists of Messages and Lists of Agents*} -theory List_Msg = Extensions: +theory List_Msg imports Extensions begin subsection{*Implementation of Lists by Messages*}