# HG changeset patch
# User wenzelm
# Date 1307209185 -7200
# Node ID a8b655d089acef1ac4875ff999c54a88fbb73386
# Parent  c6c4f997ad876fc965f3b1161ca2baaf63ac99eb
tuned secref (still dangling);

diff -r c6c4f997ad87 -r a8b655d089ac doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Jun 03 22:39:23 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Sat Jun 04 19:39:45 2011 +0200
@@ -1403,14 +1403,15 @@
 
   \item @{command (HOL) "value"}~@{text t} evaluates and prints a
     term; optionally @{text modes} can be specified, which are
-    appended to the current print mode (see also \cite{isabelle-ref}).
+    appended to the current print mode; see \secref{sec:print-modes}.
     Internally, the evaluation is performed by registered evaluators,
     which are invoked sequentially until a result is returned.
     Alternatively a specific evaluator can be selected using square
     brackets; typical evaluators use the current set of code equations
-    to normalize and include @{text simp} for fully symbolic evaluation
-    using the simplifier, @{text nbe} for \emph{normalization by evaluation}
-    and \emph{code} for code generation in SML.
+    to normalize and include @{text simp} for fully symbolic
+    evaluation using the simplifier, @{text nbe} for
+    \emph{normalization by evaluation} and \emph{code} for code
+    generation in SML.
 
   \item @{command (HOL) "quickcheck"} tests the current goal for
     counterexamples using a series of assignments for its
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
diff -r c6c4f997ad87 -r a8b655d089ac doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Jun 03 22:39:23 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Sat Jun 04 19:39:45 2011 +0200
@@ -2060,14 +2060,15 @@
 
   \item \hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}~\isa{t} evaluates and prints a
     term; optionally \isa{modes} can be specified, which are
-    appended to the current print mode (see also \cite{isabelle-ref}).
+    appended to the current print mode; see \secref{sec:print-modes}.
     Internally, the evaluation is performed by registered evaluators,
     which are invoked sequentially until a result is returned.
     Alternatively a specific evaluator can be selected using square
     brackets; typical evaluators use the current set of code equations
-    to normalize and include \isa{simp} for fully symbolic evaluation
-    using the simplifier, \isa{nbe} for \emph{normalization by evaluation}
-    and \emph{code} for code generation in SML.
+    to normalize and include \isa{simp} for fully symbolic
+    evaluation using the simplifier, \isa{nbe} for
+    \emph{normalization by evaluation} and \emph{code} for code
+    generation in SML.
 
   \item \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}} tests the current goal for
     counterexamples using a series of assignments for its
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