doc-src/IsarRef/Thy/document/Outer_Syntax.tex

   Common mathematical symbols such as \isa{{\isasymforall}} are represented in
   Isabelle as \verb|\<forall>|.  There are infinitely many Isabelle
   symbols like this, although proper presentation is left to front-end
   tools such as {\LaTeX} or Proof~General with the X-Symbol package.
   A list of standard Isabelle symbols that work well with these tools
-  is given in \cite[appendix~A]{isabelle-sys}.  Note that \verb|\<lambda>| does not belong to the \isa{letter} category, since it is
-  already used differently in the Pure term language.%
+  is given in \appref{app:symbols}.  Note that \verb|\<lambda>| does
+  not belong to the \isa{letter} category, since it is already used
+  differently in the Pure term language.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isamarkupsection{Common syntax entities%
 }