| changeset 16417 | 9bc16273c2d4 |
| parent 11250 | c8bbf4c4bc2d |
| child 23925 | ee98c2528a8f |
--- 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"