diff -r bda7527ccf05 -r cc2d676d5395 src/Doc/Tutorial/Protocol/Event.thy
--- a/src/Doc/Tutorial/Protocol/Event.thy	Wed Dec 26 16:07:28 2018 +0100
+++ b/src/Doc/Tutorial/Protocol/Event.thy	Wed Dec 26 16:25:20 2018 +0100
@@ -275,7 +275,7 @@
 done
 
 
-text\<open>For proving @{text new_keys_not_used}\<close>
+text\<open>For proving \<open>new_keys_not_used\<close>\<close>
 lemma keysFor_parts_insert:
      "[| K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) |] 
       ==> K \<in> keysFor (parts (G \<union> H)) | Key (invKey K) \<in> parts H" 
@@ -350,29 +350,29 @@
 
 text \<open>
 The system's behaviour is formalized as a set of traces of
-\emph{events}.  The most important event, @{text "Says A B X"}, expresses
+\emph{events}.  The most important event, \<open>Says A B X\<close>, expresses
 $A\to B : X$, which is the attempt by~$A$ to send~$B$ the message~$X$.
 A trace is simply a list, constructed in reverse
-using~@{text "#"}.  Other event types include reception of messages (when
+using~\<open>#\<close>.  Other event types include reception of messages (when
 we want to make it explicit) and an agent's storing a fact.
 
 Sometimes the protocol requires an agent to generate a new nonce. The
 probability that a 20-byte random number has appeared before is effectively
 zero.  To formalize this important property, the set @{term "used evs"}
-denotes the set of all items mentioned in the trace~@{text evs}.
-The function @{text used} has a straightforward
-recursive definition.  Here is the case for @{text Says} event:
+denotes the set of all items mentioned in the trace~\<open>evs\<close>.
+The function \<open>used\<close> has a straightforward
+recursive definition.  Here is the case for \<open>Says\<close> event:
 @{thm [display,indent=5] used_Says [no_vars]}
 
-The function @{text knows} formalizes an agent's knowledge.  Mostly we only
+The function \<open>knows\<close> formalizes an agent's knowledge.  Mostly we only
 care about the spy's knowledge, and @{term "knows Spy evs"} is the set of items
-available to the spy in the trace~@{text evs}.  Already in the empty trace,
+available to the spy in the trace~\<open>evs\<close>.  Already in the empty trace,
 the spy starts with some secrets at his disposal, such as the private keys
-of compromised users.  After each @{text Says} event, the spy learns the
+of compromised users.  After each \<open>Says\<close> event, the spy learns the
 message that was sent:
 @{thm [display,indent=5] knows_Spy_Says [no_vars]}
 Combinations of functions express other important
-sets of messages derived from~@{text evs}:
+sets of messages derived from~\<open>evs\<close>:
 \begin{itemize}
 \item @{term "analz (knows Spy evs)"} is everything that the spy could
 learn by decryption