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*}