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