src/HOL/Auth/TLS.ML

 (**** Secrecy Theorems ****)
 
 (*Key compromise lemma needed to prove analz_image_keys.
   No collection of keys can help the spy get new private keys.*)
 Goal "evs : tls                                      \
-\     ==> ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) = \
+\     ==> ALL KK. (Key(priK B) : analz (Key`KK Un (spies evs))) = \
 \         (priK B : KK | B : bad)";
 by (etac tls.induct 1);
 by (ALLGOALS
     (asm_simp_tac (analz_image_keys_ss
 		   addsimps certificate_def::keys_distinct)));

 \     (X : analz (G Un H))  =  (X : analz H)";
 by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
 val analz_image_keys_lemma = result();
 
 (** Strangely, the following version doesn't work:
-\ ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \
+\ ALL Z. (Nonce N : analz (Key`(sessionK`Z) Un (spies evs))) = \
 \        (Nonce N : analz (spies evs))";
 **)
 
 Goal "evs : tls ==>                                    \
 \ ALL KK. KK <= range sessionK -->                     \
-\         (Nonce N : analz (Key``KK Un (spies evs))) = \
+\         (Nonce N : analz (Key`KK Un (spies evs))) = \
 \         (Nonce N : analz (spies evs))";
 by (etac tls.induct 1);
 by (ClientKeyExch_tac 7);
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
 by (REPEAT_FIRST (rtac analz_image_keys_lemma));