--- a/doc-src/TutorialI/Protocol/Message.thy Wed Feb 24 11:55:52 2010 +0100
+++ b/doc-src/TutorialI/Protocol/Message.thy Mon Mar 01 13:40:23 2010 +0100
@@ -46,8 +46,7 @@
text{*The inverse of a symmetric key is itself; that of a public key
is the private key and vice versa*}
-constdefs
- symKeys :: "key set"
+definition symKeys :: "key set" where
"symKeys == {K. invKey K = K}"
(*>*)
@@ -92,8 +91,7 @@
"{|x, y|}" == "CONST MPair x y"
-constdefs
- keysFor :: "msg set => key set"
+definition keysFor :: "msg set => key set" where
--{*Keys useful to decrypt elements of a message set*}
"keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"