diff -r 6061ae1f90f2 -r 9bc16273c2d4 doc-src/TutorialI/Protocol/Public.thy
--- a/doc-src/TutorialI/Protocol/Public.thy	Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Protocol/Public.thy	Fri Jun 17 16:12:49 2005 +0200
@@ -8,8 +8,8 @@
 Private and public keys; initial states of agents
 *)
 
-theory Public = Event
-files ("Public_lemmas.ML"):
+theory Public imports Event
+uses ("Public_lemmas.ML") begin
 
 consts
   pubK    :: "agent => key"