--- a/doc-src/IsarRef/syntax.tex Tue Oct 24 23:32:33 2000 +0200
+++ b/doc-src/IsarRef/syntax.tex Tue Oct 24 23:34:08 2000 +0200
@@ -360,7 +360,7 @@
not checked in any way.
\indexisarant{thm}\indexisarant{prop}\indexisarant{term}
-\indexisarant{typ}\indexisarant{name}
+\indexisarant{typ}\indexisarant{text}\indexisarant{goals}
\begin{rail}
atsign lbrace antiquotation rbrace
;
@@ -370,7 +370,8 @@
'prop' options prop |
'term' options term |
'typ' options type |
- 'text' options name
+ 'text' options name |
+ 'goals' options name
;
options: '[' (option * ',') ']'
;
@@ -381,6 +382,31 @@
Note that the syntax of antiquotations may \emph{not} include source comments
\texttt{(*~\dots~*)} or verbatim text \verb|{*|~\dots~\verb|*}|.
+\begin{descr}
+\item [\texttt{{\at}{\ttlbrace}thm~$\vec a${\ttrbrace}}] prints theorems $\vec
+ a$. Note that attribute specifications may be included as well (see also
+ \S\ref{sec:syn-att}); the $no_vars$ operation (see \S\ref{sec:misc-methods})
+ would be particularly useful to suppress printing of schematic variables.
+\item [\texttt{{\at}{\ttlbrace}prop~$\phi${\ttrbrace}}] prints a well-typed
+ proposition $\phi$.
+\item [\texttt{{\at}{\ttlbrace}term~$t${\ttrbrace}}] prints a well-typed term
+ $t$.
+\item [\texttt{{\at}{\ttlbrace}typ~$\tau${\ttrbrace}}] prints a well-formed
+ type $\tau$.
+\item [\texttt{{\at}{\ttlbrace}text~$s${\ttrbrace}}] prints uninterpreted
+ source text $s$. This is particularly useful to print portions of text
+ according to the Isabelle {\LaTeX} output style, without demanding
+ well-formedness (e.g.\ small pieces of terms that cannot be parsed or
+ type-checked yet).
+\item [\texttt{{\at}{\ttlbrace}goals{\ttrbrace}}] prints the current
+ \emph{dynamic} goal state. This is only for support of tactic-emulation
+ scripts within Isar --- presentation of goal states does not conform to
+ actual human-readable proof documents.
+
+ Please do not include goal states into document output unless you really
+ know what you are doing!
+\end{descr}
+
\medskip
The following options are available to tune the output. Note that some of
@@ -406,6 +432,8 @@
rather than the actual value. Note that this does not affect
well-formedness checks of $thm$, $term$, etc. (only the $text$ antiquotation
admits arbitrary output).
+\item[$goals_limit = nat$] determines the maximum number of goals to be
+ printed.
\end{descr}
For boolean flags, ``$name = true$'' may be abbreviated as ``$name$''. All of