diff -r 4dc65845eab3 -r d8d7d1b785af doc-src/TutorialI/Protocol/Message.thy
--- 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}"