src/Doc/Tutorial/Protocol/NS_Public.thy

 Here is a detailed explanation of rule \<open>NS2\<close>.
 A trace containing an event of the form
 @{term [display,indent=5] "Says A' B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>)"}
 may be extended by an event of the form
 @{term [display,indent=5] "Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)"}
-where \<open>NB\<close> is a fresh nonce: @{term "Nonce NB \<notin> used evs2"}.
+where \<open>NB\<close> is a fresh nonce: \<^term>\<open>Nonce NB \<notin> used evs2\<close>.
 Writing the sender as \<open>A'\<close> indicates that \<open>B\<close> does not 
 know who sent the message.  Calling the trace variable \<open>evs2\<close> rather
 than simply \<open>evs\<close> helps us know where we are in a proof after many
 case-splits: every subgoal mentioning \<open>evs2\<close> involves message~2 of the
 protocol.

 (*>*)
 
 text \<open>
 Secrecy properties can be hard to prove.  The conclusion of a typical
 secrecy theorem is 
-@{term "X \<notin> analz (knows Spy evs)"}.  The difficulty arises from
+\<^term>\<open>X \<notin> analz (knows Spy evs)\<close>.  The difficulty arises from
 having to reason about \<open>analz\<close>, or less formally, showing that the spy
 can never learn~\<open>X\<close>.  Much easier is to prove that \<open>X\<close> can never
 occur at all.  Such \emph{regularity} properties are typically expressed
 using \<open>parts\<close> rather than \<open>analz\<close>.
 

 by auto
 (*>*)
 
 text \<open>
 The \<open>Fake\<close> case is proved automatically.  If
-@{term "priK A"} is in the extended trace then either (1) it was already in the
+\<^term>\<open>priK A\<close> is in the extended trace then either (1) it was already in the
 original trace or (2) it was
 generated by the spy, who must have known this key already. 
 Either way, the induction hypothesis applies.
 
 \emph{Unicity} lemmas are regularity lemmas stating that specified items

 default simplification rule that does a case
 analysis for each encrypted message on whether or not the decryption key
 is compromised.
 @{named_thms [display,indent=0,margin=50] analz_Crypt_if [no_vars] (analz_Crypt_if)}
 The simplifier has also used \<open>Spy_see_priK\<close>, proved in
-{\S}\ref{sec:regularity} above, to yield @{term "Ba \<in> bad"}.
+{\S}\ref{sec:regularity} above, to yield \<^term>\<open>Ba \<in> bad\<close>.
 
 Recall that this subgoal concerns the case
 where the last message to be sent was
 \[ 1.\quad  A'\to B'  : \comp{Na',A'}\sb{Kb'}. \]
 This message can compromise $Nb$ only if $Nb=Na'$ and $B'$ is compromised,
 allowing the spy to decrypt the message.  The Isabelle subgoal says
 precisely this, if we allow for its choice of variable names.
-Proving @{term "NB \<noteq> NAa"} is easy: \<open>NB\<close> was
+Proving \<^term>\<open>NB \<noteq> NAa\<close> is easy: \<open>NB\<close> was
 sent earlier, while \<open>NAa\<close> is fresh; formally, we have
-the assumption @{term "Nonce NAa \<notin> used evs1"}. 
+the assumption \<^term>\<open>Nonce NAa \<notin> used evs1\<close>. 
 
 Note that our reasoning concerned \<open>B\<close>'s participation in another
 run.  Agents may engage in several runs concurrently, and some attacks work
 by interleaving the messages of two runs.  With model checking, this
 possibility can cause a state-space explosion, and for us it