src/HOL/Auth/OtwayRees_AN.thy

                  Crypt (shrK B) \<lbrace>Nonce NB, Agent A, Agent B, Key KAB\<rbrace>\<rbrace>
               # evs3 \<in> otway"
 
  | OR4:  \<comment> \<open>Bob receives the Server's (?) message and compares the Nonces with
              those in the message he previously sent the Server.
-             Need @{term "B \<noteq> Server"} because we allow messages to self.\<close>
+             Need \<^term>\<open>B \<noteq> Server\<close> because we allow messages to self.\<close>
          "[| evs4 \<in> otway;  B \<noteq> Server;
              Says B Server \<lbrace>Agent A, Agent B, Nonce NA, Nonce NB\<rbrace> \<in>set evs4;
              Gets B \<lbrace>X, Crypt(shrK B)\<lbrace>Nonce NB,Agent A,Agent B,Key K\<rbrace>\<rbrace>
                \<in>set evs4 |]
           ==> Says B A X # evs4 \<in> otway"

      "[| Gets B \<lbrace>X, Crypt(shrK B) X'\<rbrace> \<in> set evs;  evs \<in> otway |]
       ==> X \<in> analz (knows Spy evs)"
 by blast
 
 
-text\<open>Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that
+text\<open>Theorems of the form \<^term>\<open>X \<notin> parts (spies 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> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"

 by (blast intro!: NA_Crypt_imp_Server_msg)
 
 
 text\<open>Crucial secrecy property: Spy does not see the keys sent in msg OR3
     Does not in itself guarantee security: an attack could violate
-    the premises, e.g. by having @{term "A=Spy"}\<close>
+    the premises, e.g. by having \<^term>\<open>A=Spy\<close>\<close>
 lemma secrecy_lemma:
      "[| A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
       ==> Says Server B
            \<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>,
              Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace>