--- a/src/HOL/Auth/KerberosIV.ML Tue Jan 09 15:22:13 2001 +0100
+++ b/src/HOL/Auth/KerberosIV.ML Tue Jan 09 15:29:17 2001 +0100
@@ -609,9 +609,9 @@
(*We take some pains to express the property
as a logical equivalence so that the simplifier can apply it.*)
-Goal "P --> (Key K : analz (Key``KK Un H)) --> (K:KK | Key K : analz H) \
+Goal "P --> (Key K : analz (Key`KK Un H)) --> (K:KK | Key K : analz H) \
\ ==> \
-\ P --> (Key K : analz (Key``KK Un H)) = (K:KK | Key K : analz H)";
+\ P --> (Key K : analz (Key`KK Un H)) = (K:KK | Key K : analz H)";
by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
qed "Key_analz_image_Key_lemma";
@@ -651,7 +651,7 @@
ORELSE' hyp_subst_tac)];
Goal "[| KK <= -(range shrK); Key K : analz (spies evs); evs: kerberos |] \
-\ ==> Key K : analz (Key `` KK Un spies evs)";
+\ ==> Key K : analz (Key ` KK Un spies evs)";
by (blast_tac (claset() addDs [impOfSubs analz_mono]) 1);
qed "analz_mono_KK";
@@ -673,7 +673,7 @@
Goal "evs : kerberos ==> \
\ (ALL SK KK. KK <= -(range shrK) --> \
\ (ALL K: KK. ~ KeyCryptKey K SK evs) --> \
-\ (Key SK : analz (Key``KK Un (spies evs))) = \
+\ (Key SK : analz (Key`KK Un (spies evs))) = \
\ (SK : KK | Key SK : analz (spies evs)))";
by (etac kerberos.induct 1);
by analz_sees_tac;