--- a/doc-src/IsarRef/Thy/Misc.thy Thu Nov 13 22:00:39 2008 +0100
+++ b/doc-src/IsarRef/Thy/Misc.thy Thu Nov 13 22:01:30 2008 +0100
@@ -48,11 +48,10 @@
the theory context; the ``@{text "!"}'' option indicates extra
verbosity.
- \item @{command "print_syntax"} prints the inner syntax of types
- and terms, depending on the current context. The output can be very
+ \item @{command "print_syntax"} prints the inner syntax of types and
+ terms, depending on the current context. The output can be very
verbose, including grammar tables and syntax translation rules. See
- \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's
- inner syntax.
+ \chref{ch:inner-syntax} for further information on inner syntax.
\item @{command "print_methods"} prints all proof methods
available in the current theory context.