src/HOL/Metis_Examples/Message.thy
changeset 35416 d8d7d1b785af
parent 35109 0015a0a99ae9
child 36553 95bdfa572cee
     1.1 --- a/src/HOL/Metis_Examples/Message.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Metis_Examples/Message.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -26,8 +26,7 @@
     1.4  text{*The inverse of a symmetric key is itself; that of a public key
     1.5        is the private key and vice versa*}
     1.6  
     1.7 -constdefs
     1.8 -  symKeys :: "key set"
     1.9 +definition symKeys :: "key set" where
    1.10    "symKeys == {K. invKey K = K}"
    1.11  
    1.12  datatype  --{*We allow any number of friendly agents*}
    1.13 @@ -55,12 +54,11 @@
    1.14    "{|x, y|}"      == "CONST MPair x y"
    1.15  
    1.16  
    1.17 -constdefs
    1.18 -  HPair :: "[msg,msg] => msg"                       ("(4Hash[_] /_)" [0, 1000])
    1.19 +definition HPair :: "[msg,msg] => msg" ("(4Hash[_] /_)" [0, 1000]) where
    1.20      --{*Message Y paired with a MAC computed with the help of X*}
    1.21      "Hash[X] Y == {| Hash{|X,Y|}, Y|}"
    1.22  
    1.23 -  keysFor :: "msg set => key set"
    1.24 +definition keysFor :: "msg set => key set" where
    1.25      --{*Keys useful to decrypt elements of a message set*}
    1.26    "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
    1.27