# HG changeset patch
# User paulson
# Date 846145843 -7200
# Node ID 7e118eb32bdc5836cb8b3416190489a3b8e21f82
# Parent  df91b1610c05d65a0526ae793e5cf18b9a8e735f
Removal of unused predicate isSpy

diff -r df91b1610c05 -r 7e118eb32bdc src/HOL/Auth/Message.thy
--- 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