diff -r 2f5edb146f7e -r 1f073030b97a doc-src/TutorialI/Protocol/protocol.tex
--- 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