src/HOL/Auth/Message.thy
changeset 2121 7e118eb32bdc
parent 2032 1bbf1bdcaf56
child 2284 80ebd1a213fd
     1.1 --- a/src/HOL/Auth/Message.thy	Thu Oct 24 10:30:17 1996 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Thu Oct 24 10:30:43 1996 +0200
     1.3 @@ -38,14 +38,6 @@
     1.4  datatype  (*We allow any number of friendly agents*)
     1.5    agent = Server | Friend nat | Spy
     1.6  
     1.7 -consts  
     1.8 -  isSpy :: agent => bool
     1.9 -
    1.10 -primrec isSpy agent
    1.11 -  isSpy_Server  "isSpy Server  = False"
    1.12 -  isSpy_Friend  "isSpy (Friend i) = False"
    1.13 -  isSpy_Spy   "isSpy Spy = True"
    1.14 -
    1.15  datatype  (*Messages are agent names, nonces, keys, pairs and encryptions*)
    1.16    msg = Agent agent
    1.17        | Nonce nat