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