diff -r 5200374fda5d -r 8b1aa4357320 doc-src/TutorialI/Protocol/document/Public.tex
--- a/doc-src/TutorialI/Protocol/document/Public.tex	Sat Nov 10 14:31:18 2007 +0100
+++ b/doc-src/TutorialI/Protocol/document/Public.tex	Sat Nov 10 14:31:20 2007 +0100
@@ -18,18 +18,16 @@
 \begin{isamarkuptext}%
 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}).%
+\isa{priK} maps agents to their private keys.  It is merely
+an abbreviation (cf.\ \S\ref{sec:abbreviations}) defined in terms of
+\isa{invKey} and \isa{pubK}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{consts}\isamarkupfalse%
-\ pubK\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}agent\ {\isacharequal}{\isachargreater}\ key{\isachardoublequoteclose}\isanewline
-\isacommand{syntax}\isamarkupfalse%
-\ priK\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}agent\ {\isacharequal}{\isachargreater}\ key{\isachardoublequoteclose}\isanewline
-\isacommand{translations}\isamarkupfalse%
-\ {\isachardoublequoteopen}priK\ x{\isachardoublequoteclose}\ {\isasymrightleftharpoons}\ {\isachardoublequoteopen}invKey{\isacharparenleft}pubK\ x{\isacharparenright}{\isachardoublequoteclose}%
+\ pubK\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}agent\ {\isasymRightarrow}\ key{\isachardoublequoteclose}\isanewline
+\isacommand{abbreviation}\isamarkupfalse%
+\ priK\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}agent\ {\isasymRightarrow}\ key{\isachardoublequoteclose}\isanewline
+\isakeyword{where}\ {\isachardoublequoteopen}priK\ x\ \ {\isasymequiv}\ \ invKey{\isacharparenleft}pubK\ x{\isacharparenright}{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \noindent
 The set \isa{bad} consists of those agents whose private keys are known to
@@ -43,7 +41,7 @@
 \isacommand{axioms}\isamarkupfalse%
 \isanewline
 \ \ inj{\isacharunderscore}pubK{\isacharcolon}\ \ \ \ \ \ \ \ {\isachardoublequoteopen}inj\ pubK{\isachardoublequoteclose}\isanewline
-\ \ priK{\isacharunderscore}neq{\isacharunderscore}pubK{\isacharcolon}\ \ \ {\isachardoublequoteopen}priK\ A\ {\isachartilde}{\isacharequal}\ pubK\ B{\isachardoublequoteclose}%
+\ \ priK{\isacharunderscore}neq{\isacharunderscore}pubK{\isacharcolon}\ \ \ {\isachardoublequoteopen}priK\ A\ {\isasymnoteq}\ pubK\ B{\isachardoublequoteclose}%
 \isadelimproof
 %
 \endisadelimproof