--- a/src/HOL/Metis_Examples/Message.thy Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Metis_Examples/Message.thy Mon Mar 01 13:40:23 2010 +0100
@@ -26,8 +26,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}"
datatype --{*We allow any number of friendly agents*}
@@ -55,12 +54,11 @@
"{|x, y|}" == "CONST MPair x y"
-constdefs
- HPair :: "[msg,msg] => msg" ("(4Hash[_] /_)" [0, 1000])
+definition HPair :: "[msg,msg] => msg" ("(4Hash[_] /_)" [0, 1000]) where
--{*Message Y paired with a MAC computed with the help of X*}
"Hash[X] Y == {| Hash{|X,Y|}, Y|}"
- 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}"