doc-src/TutorialI/Protocol/protocol.tex

 The function
 \isa{pubK} maps agents to their public keys.  The function
 \isa{priK} maps agents to their private keys.  It is defined in terms of
 \isa{invKey} and \isa{pubK} by a translation; therefore \isa{priK} is
 not a proper constant, so we declare it using \isacommand{syntax}
+(cf.\ \S\ref{sec:syntax-translations}).
 \begin{isabelle}
 \isacommand{consts}\ \,pubK\ \ \ \ ::\ "agent\ =>\ key"\isanewline
 \isacommand{syntax}\ priK\ \ \ \ ::\ "agent\ =>\ key"\isanewline
 \isacommand{translations}\ \ \ \ "priK\ x"\ \ \isasymrightleftharpoons\ \ "invKey(pubK\ x)"
 \end{isabelle}