src/Doc/Tutorial/Protocol/Public.thy

 begin
 (*>*)
 
 text \<open>
 The function
-@{text pubK} maps agents to their public keys.  The function
-@{text priK} maps agents to their private keys.  It is merely
+\<open>pubK\<close> maps agents to their public keys.  The function
+\<open>priK\<close> maps agents to their private keys.  It is merely
 an abbreviation (cf.\ \S\ref{sec:abbreviations}) defined in terms of
-@{text invKey} and @{text pubK}.
+\<open>invKey\<close> and \<open>pubK\<close>.
 \<close>
 
 consts pubK :: "agent \<Rightarrow> key"
 abbreviation priK :: "agent \<Rightarrow> key"
 where "priK x  \<equiv>  invKey(pubK x)"

 end
 (*>*)
 
 text \<open>
 \noindent
-The set @{text bad} consists of those agents whose private keys are known to
+The set \<open>bad\<close> consists of those agents whose private keys are known to
 the spy.
 
 Two axioms are asserted about the public-key cryptosystem. 
 No two agents have the same public key, and no private key equals
 any public key.