doc-src/TutorialI/Protocol/Public.thy
changeset 16417 9bc16273c2d4
parent 11250 c8bbf4c4bc2d
child 23925 ee98c2528a8f
     1.1 --- a/doc-src/TutorialI/Protocol/Public.thy	Fri Jun 17 11:35:35 2005 +0200
     1.2 +++ b/doc-src/TutorialI/Protocol/Public.thy	Fri Jun 17 16:12:49 2005 +0200
     1.3 @@ -8,8 +8,8 @@
     1.4  Private and public keys; initial states of agents
     1.5  *)
     1.6  
     1.7 -theory Public = Event
     1.8 -files ("Public_lemmas.ML"):
     1.9 +theory Public imports Event
    1.10 +uses ("Public_lemmas.ML") begin
    1.11  
    1.12  consts
    1.13    pubK    :: "agent => key"