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