--- a/doc-src/IsarRef/syntax.tex Wed Oct 25 18:34:10 2000 +0200
+++ b/doc-src/IsarRef/syntax.tex Wed Oct 25 18:35:01 2000 +0200
@@ -337,6 +337,15 @@
\subsection{Antiquotations}\label{sec:antiq}
+\begin{matharray}{rcl}
+ thm & : & \isarantiq \\
+ prop & : & \isarantiq \\
+ term & : & \isarantiq \\
+ typ & : & \isarantiq \\
+ text & : & \isarantiq \\
+ goals & : & \isarantiq \\
+\end{matharray}
+
The text body of formal comments (see also \S\ref{sec:comments}) may contain
antiquotations of logical entities, such as theorems, terms and types, which
are to be presented in the final output produced by the Isabelle document
@@ -352,13 +361,6 @@
statement where all schematic variables have been replaced by fixed ones,
which are better readable.
-Antiquotations do not only spare the author from tedious typing, but also
-achieve some degree of consistency-checking of informal explanations with
-formal developments, since well-formedness of terms and types with respect to
-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{text}\indexisarant{goals}
\begin{rail}
@@ -371,7 +373,7 @@
'term' options term |
'typ' options type |
'text' options name |
- 'goals' options name
+ 'goals' options
;
options: '[' (option * ',') ']'
;
@@ -383,25 +385,20 @@
\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.
+\item [$\at\{thm~\vec a\}$] 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 [$\at\{prop~\phi\}$] prints a well-typed proposition $\phi$.
+\item [$\at\{term~t\}$] prints a well-typed term $t$.
+\item [$\at\{typ~\tau\}$] prints a well-formed type $\tau$.
+\item [$\at\{text~s\}$] 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 [$\at\{goals\}$] 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!
@@ -409,7 +406,7 @@
\medskip
-The following options are available to tune the output. Note that some of
+The following options are available to tune the output. Note that most of
these coincide with ML flags of the same names (see also \cite{isabelle-ref}).
\begin{descr}
\item[$show_types = bool$ and $show_sorts = bool$] control printing of
@@ -439,6 +436,10 @@
For boolean flags, ``$name = true$'' may be abbreviated as ``$name$''. All of
the above flags are disabled by default, unless changed from ML.
+\medskip Note that antiquotations do not only spare the author from tedious
+typing, but also achieve some degree of consistency-checking of informal
+explanations with formal developments, since well-formedness of terms and
+types with respect to the current theory or proof context can be ensured.
%%% Local Variables:
%%% mode: latex