Removal of unused predicate isSpy
authorpaulson
Thu Oct 24 10:30:43 1996 +0200 (1996-10-24)
changeset 21217e118eb32bdc
parent 2120 df91b1610c05
child 2122 cb302f6c9c06
Removal of unused predicate isSpy
src/HOL/Auth/Message.thy
     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