doc-src/TutorialI/Protocol/Message.thy
changeset 42765 aec61b60ff7b
parent 42475 f830a72b27ed
child 42793 88bee9f6eec7
--- a/doc-src/TutorialI/Protocol/Message.thy	Thu May 12 16:58:55 2011 +0200
+++ b/doc-src/TutorialI/Protocol/Message.thy	Thu May 12 17:17:57 2011 +0200
@@ -32,7 +32,7 @@
 the matching private key, and vice versa:
 *}
 
-types key = nat
+type_synonym key = nat
 consts invKey :: "key \<Rightarrow> key"
 (*<*)
 consts all_symmetric :: bool        --{*true if all keys are symmetric*}