# HG changeset patch
# User wenzelm
# Date 972491701 -7200
# Node ID 209f502b55f79a7758a76fbf56dd32459bbefd78
# Parent  ccdbf06579827b0ebeccdf53b0b4082b08197c86
improved antiquotations;

diff -r ccdbf0657982 -r 209f502b55f7 doc-src/IsarRef/syntax.tex
--- 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