# HG changeset patch
# User bulwahn
# Date 1309509951 -7200
# Node ID 7afbaf5a406b33f3e43c3a6c79443761026af4ba
# Parent  c32144b8baba1994207d2d7cfcb9e165183d6f5f
adding a minimalistic documentation of the value antiquotation in the Isar reference manual

diff -r c32144b8baba -r 7afbaf5a406b NEWS
--- a/NEWS	Fri Jul 01 10:45:49 2011 +0200
+++ b/NEWS	Fri Jul 01 10:45:51 2011 +0200
@@ -126,6 +126,8 @@
 * Antiquotation @{rail} layouts railroad syntax diagrams, see also
 isar-ref manual.
 
+* Antiquotation @{value} evaluates the given term and presents its result.
+
 * Localized \isabellestyle switch can be used within blocks or groups
 like this:
 
diff -r c32144b8baba -r 7afbaf5a406b doc-src/IsarRef/Thy/Document_Preparation.thy
--- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Fri Jul 01 10:45:49 2011 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Fri Jul 01 10:45:51 2011 +0200
@@ -188,6 +188,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 term_type} options styles @{syntax term} |
       @@{antiquotation typeof} options styles @{syntax term} |
       @@{antiquotation const} options @{syntax term} |
@@ -236,6 +237,8 @@
   @{text "\<phi>"} by method @{text m} and prints the original @{text "\<phi>"}.
 
   \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 "@{term_type t}"} prints a well-typed term @{text "t"}
   annotated with its type.
diff -r c32144b8baba -r 7afbaf5a406b doc-src/IsarRef/Thy/document/Document_Preparation.tex
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Fri Jul 01 10:45:49 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Fri Jul 01 10:45:51 2011 +0200
@@ -235,7 +235,7 @@
 \rail@nont{\isa{antiquotation}}[]
 \rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]
 \rail@end
-\rail@begin{22}{\indexdef{}{syntax}{antiquotation}\hypertarget{syntax.antiquotation}{\hyperlink{syntax.antiquotation}{\mbox{\isa{antiquotation}}}}}
+\rail@begin{23}{\indexdef{}{syntax}{antiquotation}\hypertarget{syntax.antiquotation}{\hyperlink{syntax.antiquotation}{\mbox{\isa{antiquotation}}}}}
 \rail@bar
 \rail@term{\hyperlink{antiquotation.theory}{\mbox{\isa{theory}}}}[]
 \rail@nont{\isa{options}}[]
@@ -266,66 +266,71 @@
 \rail@nont{\isa{styles}}[]
 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
 \rail@nextbar{6}
-\rail@term{\hyperlink{antiquotation.term-type}{\mbox{\isa{term{\isaliteral{5F}{\isacharunderscore}}type}}}}[]
+\rail@term{\hyperlink{antiquotation.value}{\mbox{\isa{value}}}}[]
 \rail@nont{\isa{options}}[]
 \rail@nont{\isa{styles}}[]
 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
 \rail@nextbar{7}
-\rail@term{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}}[]
+\rail@term{\hyperlink{antiquotation.term-type}{\mbox{\isa{term{\isaliteral{5F}{\isacharunderscore}}type}}}}[]
 \rail@nont{\isa{options}}[]
 \rail@nont{\isa{styles}}[]
 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
 \rail@nextbar{8}
+\rail@term{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}}[]
+\rail@nont{\isa{options}}[]
+\rail@nont{\isa{styles}}[]
+\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
+\rail@nextbar{9}
 \rail@term{\hyperlink{antiquotation.const}{\mbox{\isa{const}}}}[]
 \rail@nont{\isa{options}}[]
 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@nextbar{9}
+\rail@nextbar{10}
 \rail@term{\hyperlink{antiquotation.abbrev}{\mbox{\isa{abbrev}}}}[]
 \rail@nont{\isa{options}}[]
 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@nextbar{10}
+\rail@nextbar{11}
 \rail@term{\hyperlink{antiquotation.typ}{\mbox{\isa{typ}}}}[]
 \rail@nont{\isa{options}}[]
 \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
-\rail@nextbar{11}
+\rail@nextbar{12}
 \rail@term{\hyperlink{antiquotation.type}{\mbox{\isa{type}}}}[]
 \rail@nont{\isa{options}}[]
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextbar{12}
+\rail@nextbar{13}
 \rail@term{\hyperlink{antiquotation.class}{\mbox{\isa{class}}}}[]
 \rail@nont{\isa{options}}[]
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextbar{13}
-\rail@term{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}}[]
-\rail@nont{\isa{options}}[]
-\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@nextbar{14}
+\rail@term{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}}[]
+\rail@nont{\isa{options}}[]
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
+\rail@nextbar{15}
 \rail@term{\hyperlink{antiquotation.goals}{\mbox{\isa{goals}}}}[]
 \rail@nont{\isa{options}}[]
-\rail@nextbar{15}
+\rail@nextbar{16}
 \rail@term{\hyperlink{antiquotation.subgoals}{\mbox{\isa{subgoals}}}}[]
 \rail@nont{\isa{options}}[]
-\rail@nextbar{16}
+\rail@nextbar{17}
 \rail@term{\hyperlink{antiquotation.prf}{\mbox{\isa{prf}}}}[]
 \rail@nont{\isa{options}}[]
 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
-\rail@nextbar{17}
+\rail@nextbar{18}
 \rail@term{\hyperlink{antiquotation.full-prf}{\mbox{\isa{full{\isaliteral{5F}{\isacharunderscore}}prf}}}}[]
 \rail@nont{\isa{options}}[]
 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
-\rail@nextbar{18}
+\rail@nextbar{19}
 \rail@term{\hyperlink{antiquotation.ML}{\mbox{\isa{ML}}}}[]
 \rail@nont{\isa{options}}[]
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextbar{19}
+\rail@nextbar{20}
 \rail@term{\hyperlink{antiquotation.ML-type}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}type}}}}[]
 \rail@nont{\isa{options}}[]
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextbar{20}
+\rail@nextbar{21}
 \rail@term{\hyperlink{antiquotation.ML-struct}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}struct}}}}[]
 \rail@nont{\isa{options}}[]
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextbar{21}
+\rail@nextbar{22}
 \rail@term{\hyperlink{antiquotation.file}{\mbox{\isa{file}}}}[]
 \rail@nont{\isa{options}}[]
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
@@ -390,6 +395,8 @@
   \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} by method \isa{m} and prints the original \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}}.
 
   \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}}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.