--- a/doc-src/IsarRef/Thy/Document_Preparation.thy Fri Jul 01 14:17:02 2011 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Fri Jul 01 15:14:44 2011 +0200
@@ -179,6 +179,7 @@
antiquotations are checked within the current theory or proof
context.
+ %% FIXME less monolithic presentation, move to individual sections!?
@{rail "
'@{' antiquotation '}'
;
@@ -188,7 +189,7 @@
@@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? |
@@{antiquotation prop} options styles @{syntax prop} |
@@{antiquotation term} options styles @{syntax term} |
- @@{antiquotation value} options styles @{syntax term} |
+ @@{antiquotation (HOL) value} options styles @{syntax term} |
@@{antiquotation term_type} options styles @{syntax term} |
@@{antiquotation typeof} options styles @{syntax term} |
@@{antiquotation const} options @{syntax term} |
@@ -238,7 +239,8 @@
\item @{text "@{term t}"} prints a well-typed term @{text "t"}.
- \item @{text "@{value t}"} evaluates a term @{text "t"} and prints its result.
+ \item @{text "@{value t}"} evaluates a term @{text "t"} and prints
+ its result, see also @{command_ref (HOL) value}.
\item @{text "@{term_type t}"} prints a well-typed term @{text "t"}
annotated with its type.
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Fri Jul 01 14:17:02 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Fri Jul 01 15:14:44 2011 +0200
@@ -229,6 +229,7 @@
antiquotations are checked within the current theory or proof
context.
+ %% FIXME less monolithic presentation, move to individual sections!?
\begin{railoutput}
\rail@begin{1}{}
\rail@term{\isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}}}[]
@@ -266,7 +267,7 @@
\rail@nont{\isa{styles}}[]
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
\rail@nextbar{6}
-\rail@term{\hyperlink{antiquotation.value}{\mbox{\isa{value}}}}[]
+\rail@term{\hyperlink{antiquotation.HOL.value}{\mbox{\isa{value}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\isa{styles}}[]
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
@@ -396,7 +397,8 @@
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}term\ t{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} prints a well-typed term \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}}.
- \item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}value\ t{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} evaluates a term \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}} and prints its result.
+ \item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}value\ t{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} evaluates a term \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}} and prints
+ its result, see also \indexref{HOL}{command}{value}\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}.
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}term{\isaliteral{5F}{\isacharunderscore}}type\ t{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} prints a well-typed term \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}}
annotated with its type.