diff -r c6c4f997ad87 -r a8b655d089ac doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- 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