--- a/src/HOL/Auth/Public.thy Tue Jan 09 15:22:13 2001 +0100
+++ b/src/HOL/Auth/Public.thy Tue Jan 09 15:29:17 2001 +0100
@@ -22,11 +22,11 @@
primrec
(*Agents know their private key and all public keys*)
initState_Server "initState Server =
- insert (Key (priK Server)) (Key `` range pubK)"
+ insert (Key (priK Server)) (Key ` range pubK)"
initState_Friend "initState (Friend i) =
- insert (Key (priK (Friend i))) (Key `` range pubK)"
+ insert (Key (priK (Friend i))) (Key ` range pubK)"
initState_Spy "initState Spy =
- (Key``invKey``pubK``bad) Un (Key `` range pubK)"
+ (Key`invKey`pubK`bad) Un (Key ` range pubK)"
rules