src/HOL/Auth/Kerberos_BAN.ML

 
 (** Session keys are not used to encrypt other session keys **)
 
 Goal "evs : kerberos_ban ==>                          \
 \  ALL K KK. KK <= - (range shrK) -->                 \
-\         (Key K : analz (Key``KK Un (spies evs))) =  \
+\         (Key K : analz (Key`KK Un (spies evs))) =  \
 \         (K : KK | Key K : analz (spies evs))";
 by (etac kerberos_ban.induct 1);
 by analz_spies_tac;
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
 by (REPEAT_FIRST (rtac analz_image_freshK_lemma));