src/HOL/Auth/Smartcard/ShoupRubinBella.thy

       "evs \<in> srb \<Longrightarrow> Outpts (Card Server) P X \<notin> set evs"
 apply (erule srb.induct)
 apply auto
 done
 
-text\<open>@{term step2_integrity} also is a reliability theorem\<close>
+text\<open>\<^term>\<open>step2_integrity\<close> also is a reliability theorem\<close>
 lemma Says_Server_message_form: 
      "\<lbrakk> Says Server A \<lbrace>Pk, Certificate\<rbrace> \<in> set evs;  
          evs \<in> srb \<rbrakk>                   
      \<Longrightarrow> \<exists> B. Pk = Nonce (Pairkey(A,B)) \<and>  
          Certificate = Crypt (shrK A) \<lbrace>Nonce (Pairkey(A,B)), Agent B\<rbrace>"

 apply (blast dest!: Outpts_Server_not_evs)+
 done
 (*cannot be made useful to A in form of a Gets event*)
 
 text\<open>
-  step4integrity is @{term Outpts_A_Card_form_4}
-
-  step7integrity is @{term Outpts_B_Card_form_7}
+  step4integrity is \<^term>\<open>Outpts_A_Card_form_4\<close>
+
+  step7integrity is \<^term>\<open>Outpts_B_Card_form_7\<close>
 \<close>
 
 lemma step8_integrity: 
      "\<lbrakk> Says B A \<lbrace>Nonce Nb, Certificate\<rbrace> \<in> set evs;  
          B \<noteq> Server; B \<noteq> Spy; evs \<in> srb \<rbrakk>                   

 prefer 18 apply (fastforce dest: Outpts_A_Card_form_10)
 apply auto
 done
 
 
-text\<open>step9integrity is @{term Inputs_A_Card_form_9}
-        step10integrity is @{term Outpts_A_Card_form_10}.
+text\<open>step9integrity is \<^term>\<open>Inputs_A_Card_form_9\<close>
+        step10integrity is \<^term>\<open>Outpts_A_Card_form_10\<close>.
 \<close>
 
 
 lemma step11_integrity: 
      "\<lbrakk> Says A B (Certificate) \<in> set evs;