doc-src/TutorialI/Documents/Documents.thy

   user-interface of Proof~General + X-Symbol and the Isabelle document
   processor (see \S\ref{sec:document-preparation}) display the
   \verb,\,\verb,<forall>, symbol as~@{text \<forall>}.
 
   A list of standard Isabelle symbols is given in
-  \cite[appendix~A]{isabelle-sys}.  You may introduce your own
+  \cite{isabelle-isar-ref}.  You may introduce your own
   interpretation of further symbols by configuring the appropriate
   front-end tool accordingly, e.g.\ by defining certain {\LaTeX}
   macros (see also \S\ref{sec:doc-prep-symbols}).  There are also a
   few predefined control symbols, such as \verb,\,\verb,<^sub>, and
   \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent

   As has been pointed out before (\S\ref{sec:syntax-symbols}),
   Isabelle symbols are the smallest syntactic entities --- a
   straightforward generalization of ASCII characters.  While Isabelle
   does not impose any interpretation of the infinite collection of
   named symbols, {\LaTeX} documents use canonical glyphs for certain
-  standard symbols \cite[appendix~A]{isabelle-sys}.
+  standard symbols \cite{isabelle-isar-ref}.
 
   The {\LaTeX} code produced from Isabelle text follows a simple
   scheme.  You can tune the final appearance by redefining certain
   macros, say in \texttt{root.tex} of the document.