--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Fri Jun 03 22:39:23 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sat Jun 04 19:39:45 2011 +0200
@@ -151,8 +151,8 @@
\end{description}
All of the diagnostic commands above admit a list of \isa{modes}
- to be specified, which is appended to the current print mode (see
- also \cite{isabelle-ref}). Thus the output behavior may be modified
+ to be specified, which is appended to the current print mode; see
+ \secref{sec:print-modes}. Thus the output behavior may be modified
according particular print mode features. For example, \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}latex\ xsymbols{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} would print the current proof state
with mathematical symbols and special characters represented in
{\LaTeX} source, according to the Isabelle style