src/HOL/Auth/Yahalom_Bad.thy

 
 lemmas YM4_parts_knows_Spy =
        YM4_analz_knows_Spy [THEN analz_into_parts]
 
 
-text\<open>Theorems of the form @{term "X \<notin> parts (knows Spy evs)"} imply 
+text\<open>Theorems of the form \<^term>\<open>X \<notin> parts (knows Spy evs)\<close> imply 
             that NOBODY sends messages containing X!\<close>
 
 text\<open>Spy never sees a good agent's shared key!\<close>
 lemma Spy_see_shrK [simp]:
      "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"

        frule_tac [6] YM4_parts_knows_Spy)
 apply (analz_mono_contra, simp_all)
 txt\<open>Fake\<close>
 apply blast
 txt\<open>YM3: by \<open>new_keys_not_used\<close>, the message
-   @{term "Crypt K (Nonce NB)"} could not exist\<close>
+   \<^term>\<open>Crypt K (Nonce NB)\<close> could not exist\<close>
 apply (force dest!: Crypt_imp_keysFor)
-txt\<open>YM4: was @{term "Crypt K (Nonce NB)"} the very last message?
+txt\<open>YM4: was \<^term>\<open>Crypt K (Nonce NB)\<close> the very last message?
     If not, use the induction hypothesis\<close>
 apply (simp add: ex_disj_distrib)
 txt\<open>yes: apply unicity of session keys\<close>
 apply (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK
                     Crypt_Spy_analz_bad