
diff -r c6c4f997ad87 -r a8b655d089ac doc-src/IsarRef/Thy/Inner_Syntax.thy
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Fri Jun 03 22:39:23 2011 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sat Jun 04 19:39:45 2011 +0200
@@ -77,8 +77,8 @@
   \end{description}
 
   All of the diagnostic commands above admit a list of @{text 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, @{command
   "pr"}~@{text "(latex xsymbols)"} would print the current proof state
   with mathematical symbols and special characters represented in




