# HG changeset patch
# User wenzelm
# Date 1309526084 -7200
# Node ID 1c43134ff98806dd89cf8f0faa0739d87cf984ba
# Parent  5e22da27b5facab3dea01a25feb6152aafa2f98b
tuned;

diff -r 5e22da27b5fa -r 1c43134ff988 doc-src/IsarRef/Thy/Document_Preparation.thy
--- 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.
diff -r 5e22da27b5fa -r 1c43134ff988 doc-src/IsarRef/Thy/document/Document_Preparation.tex
--- 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.