doc-src/IsarRef/syntax.tex

 the current theory or proof context can be ensured.  The $text$ antiquotation
 is an exception to this rule: it prints an uninterpreted text argument that is
 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
   ;
 
   antiquotation:
     'thm' options thmrefs |
     'prop' options prop |
     'term' options term |
     'typ' options type |
-    'text' options name
+    'text' options name |
+    'goals' options name
   ;
   options: '[' (option * ',') ']'
   ;
   option: name | name '=' name
   ;
 \end{rail}
 
 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
 these coincide with ML flags of the same names (see also \cite{isabelle-ref}).

   pretty printing of display material.
 \item[$source = bool$] prints the source text of the antiquotation arguments,
   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
 the above flags are disabled by default, unless changed from ML.