adding a minimalistic documentation of the value antiquotation in the Isar reference manual
authorbulwahn
Fri Jul 01 10:45:51 2011 +0200 (2011-07-01)
changeset 436137afbaf5a406b
parent 43612 c32144b8baba
child 43614 2c741b50d4b7
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
NEWS
doc-src/IsarRef/Thy/Document_Preparation.thy
doc-src/IsarRef/Thy/document/Document_Preparation.tex
     1.1 --- a/NEWS	Fri Jul 01 10:45:49 2011 +0200
     1.2 +++ b/NEWS	Fri Jul 01 10:45:51 2011 +0200
     1.3 @@ -126,6 +126,8 @@
     1.4  * Antiquotation @{rail} layouts railroad syntax diagrams, see also
     1.5  isar-ref manual.
     1.6  
     1.7 +* Antiquotation @{value} evaluates the given term and presents its result.
     1.8 +
     1.9  * Localized \isabellestyle switch can be used within blocks or groups
    1.10  like this:
    1.11  
     2.1 --- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Fri Jul 01 10:45:49 2011 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Fri Jul 01 10:45:51 2011 +0200
     2.3 @@ -188,6 +188,7 @@
     2.4        @@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? |
     2.5        @@{antiquotation prop} options styles @{syntax prop} |
     2.6        @@{antiquotation term} options styles @{syntax term} |
     2.7 +      @@{antiquotation value} options styles @{syntax term} |
     2.8        @@{antiquotation term_type} options styles @{syntax term} |
     2.9        @@{antiquotation typeof} options styles @{syntax term} |
    2.10        @@{antiquotation const} options @{syntax term} |
    2.11 @@ -236,6 +237,8 @@
    2.12    @{text "\<phi>"} by method @{text m} and prints the original @{text "\<phi>"}.
    2.13  
    2.14    \item @{text "@{term t}"} prints a well-typed term @{text "t"}.
    2.15 +  
    2.16 +  \item @{text "@{value t}"} evaluates a term @{text "t"} and prints its result.
    2.17  
    2.18    \item @{text "@{term_type t}"} prints a well-typed term @{text "t"}
    2.19    annotated with its type.
     3.1 --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Fri Jul 01 10:45:49 2011 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Fri Jul 01 10:45:51 2011 +0200
     3.3 @@ -235,7 +235,7 @@
     3.4  \rail@nont{\isa{antiquotation}}[]
     3.5  \rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]
     3.6  \rail@end
     3.7 -\rail@begin{22}{\indexdef{}{syntax}{antiquotation}\hypertarget{syntax.antiquotation}{\hyperlink{syntax.antiquotation}{\mbox{\isa{antiquotation}}}}}
     3.8 +\rail@begin{23}{\indexdef{}{syntax}{antiquotation}\hypertarget{syntax.antiquotation}{\hyperlink{syntax.antiquotation}{\mbox{\isa{antiquotation}}}}}
     3.9  \rail@bar
    3.10  \rail@term{\hyperlink{antiquotation.theory}{\mbox{\isa{theory}}}}[]
    3.11  \rail@nont{\isa{options}}[]
    3.12 @@ -266,66 +266,71 @@
    3.13  \rail@nont{\isa{styles}}[]
    3.14  \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
    3.15  \rail@nextbar{6}
    3.16 -\rail@term{\hyperlink{antiquotation.term-type}{\mbox{\isa{term{\isaliteral{5F}{\isacharunderscore}}type}}}}[]
    3.17 +\rail@term{\hyperlink{antiquotation.value}{\mbox{\isa{value}}}}[]
    3.18  \rail@nont{\isa{options}}[]
    3.19  \rail@nont{\isa{styles}}[]
    3.20  \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
    3.21  \rail@nextbar{7}
    3.22 -\rail@term{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}}[]
    3.23 +\rail@term{\hyperlink{antiquotation.term-type}{\mbox{\isa{term{\isaliteral{5F}{\isacharunderscore}}type}}}}[]
    3.24  \rail@nont{\isa{options}}[]
    3.25  \rail@nont{\isa{styles}}[]
    3.26  \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
    3.27  \rail@nextbar{8}
    3.28 +\rail@term{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}}[]
    3.29 +\rail@nont{\isa{options}}[]
    3.30 +\rail@nont{\isa{styles}}[]
    3.31 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
    3.32 +\rail@nextbar{9}
    3.33  \rail@term{\hyperlink{antiquotation.const}{\mbox{\isa{const}}}}[]
    3.34  \rail@nont{\isa{options}}[]
    3.35  \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
    3.36 -\rail@nextbar{9}
    3.37 +\rail@nextbar{10}
    3.38  \rail@term{\hyperlink{antiquotation.abbrev}{\mbox{\isa{abbrev}}}}[]
    3.39  \rail@nont{\isa{options}}[]
    3.40  \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
    3.41 -\rail@nextbar{10}
    3.42 +\rail@nextbar{11}
    3.43  \rail@term{\hyperlink{antiquotation.typ}{\mbox{\isa{typ}}}}[]
    3.44  \rail@nont{\isa{options}}[]
    3.45  \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
    3.46 -\rail@nextbar{11}
    3.47 +\rail@nextbar{12}
    3.48  \rail@term{\hyperlink{antiquotation.type}{\mbox{\isa{type}}}}[]
    3.49  \rail@nont{\isa{options}}[]
    3.50  \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    3.51 -\rail@nextbar{12}
    3.52 +\rail@nextbar{13}
    3.53  \rail@term{\hyperlink{antiquotation.class}{\mbox{\isa{class}}}}[]
    3.54  \rail@nont{\isa{options}}[]
    3.55  \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    3.56 -\rail@nextbar{13}
    3.57 -\rail@term{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}}[]
    3.58 -\rail@nont{\isa{options}}[]
    3.59 -\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    3.60  \rail@nextbar{14}
    3.61 +\rail@term{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}}[]
    3.62 +\rail@nont{\isa{options}}[]
    3.63 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    3.64 +\rail@nextbar{15}
    3.65  \rail@term{\hyperlink{antiquotation.goals}{\mbox{\isa{goals}}}}[]
    3.66  \rail@nont{\isa{options}}[]
    3.67 -\rail@nextbar{15}
    3.68 +\rail@nextbar{16}
    3.69  \rail@term{\hyperlink{antiquotation.subgoals}{\mbox{\isa{subgoals}}}}[]
    3.70  \rail@nont{\isa{options}}[]
    3.71 -\rail@nextbar{16}
    3.72 +\rail@nextbar{17}
    3.73  \rail@term{\hyperlink{antiquotation.prf}{\mbox{\isa{prf}}}}[]
    3.74  \rail@nont{\isa{options}}[]
    3.75  \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
    3.76 -\rail@nextbar{17}
    3.77 +\rail@nextbar{18}
    3.78  \rail@term{\hyperlink{antiquotation.full-prf}{\mbox{\isa{full{\isaliteral{5F}{\isacharunderscore}}prf}}}}[]
    3.79  \rail@nont{\isa{options}}[]
    3.80  \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
    3.81 -\rail@nextbar{18}
    3.82 +\rail@nextbar{19}
    3.83  \rail@term{\hyperlink{antiquotation.ML}{\mbox{\isa{ML}}}}[]
    3.84  \rail@nont{\isa{options}}[]
    3.85  \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    3.86 -\rail@nextbar{19}
    3.87 +\rail@nextbar{20}
    3.88  \rail@term{\hyperlink{antiquotation.ML-type}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}type}}}}[]
    3.89  \rail@nont{\isa{options}}[]
    3.90  \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    3.91 -\rail@nextbar{20}
    3.92 +\rail@nextbar{21}
    3.93  \rail@term{\hyperlink{antiquotation.ML-struct}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}struct}}}}[]
    3.94  \rail@nont{\isa{options}}[]
    3.95  \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    3.96 -\rail@nextbar{21}
    3.97 +\rail@nextbar{22}
    3.98  \rail@term{\hyperlink{antiquotation.file}{\mbox{\isa{file}}}}[]
    3.99  \rail@nont{\isa{options}}[]
   3.100  \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
   3.101 @@ -390,6 +395,8 @@
   3.102    \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}}}.
   3.103  
   3.104    \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}}}.
   3.105 +  
   3.106 +  \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.
   3.107  
   3.108    \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}}}
   3.109    annotated with its type.