src/HOL/SET_Protocol/Message_SET.thy
changeset 35416 d8d7d1b785af
parent 35068 544867142ea4
child 35703 29cb504abbb5
     1.1 --- a/src/HOL/SET_Protocol/Message_SET.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/SET_Protocol/Message_SET.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -48,8 +48,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  text{*Agents. We allow any number of certification authorities, cardholders
    1.13 @@ -81,8 +80,7 @@
    1.14    "{|x, y|}"      == "CONST MPair x y"
    1.15  
    1.16  
    1.17 -constdefs
    1.18 -  nat_of_agent :: "agent => nat"
    1.19 +definition nat_of_agent :: "agent => nat" where
    1.20     "nat_of_agent == agent_case (curry nat2_to_nat 0)
    1.21                                 (curry nat2_to_nat 1)
    1.22                                 (curry nat2_to_nat 2)