src/HOL/Auth/Yahalom_Bad.ML

 
 (** Session keys are not used to encrypt other session keys **)
 
 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;
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
 by (REPEAT_FIRST (rtac analz_image_freshK_lemma));