--- a/src/HOL/Auth/Yahalom.ML Tue Jan 09 15:22:13 2001 +0100
+++ b/src/HOL/Auth/Yahalom.ML Tue Jan 09 15:29:17 2001 +0100
@@ -147,7 +147,7 @@
Goal "evs : yahalom ==> \
\ ALL K KK. KK <= - (range shrK) --> \
-\ (Key K : analz (Key``KK Un (knows Spy evs))) = \
+\ (Key K : analz (Key`KK Un (knows Spy evs))) = \
\ (K : KK | Key K : analz (knows Spy evs))";
by (etac yahalom.induct 1);
by analz_knows_Spy_tac;
@@ -367,7 +367,7 @@
Goal "evs : yahalom ==> \
\ (ALL KK. KK <= - (range shrK) --> \
\ (ALL K: KK. ~ KeyWithNonce K NB evs) --> \
-\ (Nonce NB : analz (Key``KK Un (knows Spy evs))) = \
+\ (Nonce NB : analz (Key`KK Un (knows Spy evs))) = \
\ (Nonce NB : analz (knows Spy evs)))";
by (etac yahalom.induct 1);
by analz_knows_Spy_tac;