diff -r e33b47e4246d -r c0844a30ea4e src/HOL/Auth/KerberosIV.ML --- 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;