--- 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