--- a/doc-src/TutorialI/Protocol/protocol.tex Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Protocol/protocol.tex Fri Jan 18 18:30:19 2002 +0100
@@ -324,6 +324,7 @@
\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