--- 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