doc-src/TutorialI/Protocol/Event.thy

--- a/doc-src/TutorialI/Protocol/Event.thy	Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Protocol/Event.thy	Fri Jun 17 16:12:49 2005 +0200
@@ -11,8 +11,8 @@
     stores are visible to him
 *)
 
-theory Event = Message
-files ("Event_lemmas.ML"):
+theory Event imports Message
+uses ("Event_lemmas.ML") begin
 
 consts  (*Initial states of agents -- parameter of the construction*)
   initState :: "agent => msg set"