# HG changeset patch
# User wenzelm
# Date 962311044 -7200
# Node ID 3a44c828be1d0ddceb502400f9f2fb27db0b8e6b
# Parent  7a1a856f0571cd9771eb9b52eb1e32e6569b781e
syntax: renamed 'thmname' to 'thmbind';
added subsection{Antiquotations};

diff -r 7a1a856f0571 -r 3a44c828be1d doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Thu Jun 29 22:36:45 2000 +0200
+++ b/doc-src/IsarRef/syntax.tex	Thu Jun 29 22:37:24 2000 +0200
@@ -277,16 +277,16 @@
 \begin{rail}
   axmdecl: name attributes? ':'
   ;
-  thmdecl: thmname ':'
+  thmdecl: thmbind ':'
   ;
-  thmdef: thmname '='
+  thmdef: thmbind '='
   ;
   thmref: nameref attributes?
   ;
   thmrefs: thmref +
   ;
 
-  thmname: name attributes | name | attributes
+  thmbind: name attributes | name | attributes
   ;
 \end{rail}
 
@@ -320,6 +320,69 @@
 \end{rail}
 
 
+\subsection{Antiquotations}\label{sec:antiq}
+
+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
+preparation system (see also \S\ref{sec:document-prep}).
+
+Thus embedding something like
+\texttt{{\at}{\ttlbrace}term[show_types]~"f(x)~=~a~+~x"{\ttrbrace}} within
+some text block would cause
+\isa{(f{\isasymColon}'a~{\isasymRightarrow}~'a)~(x{\isasymColon}'a)~=~(a{\isasymColon}'a)~+~x}
+to appear in the final {\LaTeX} document.
+
+\medskip
+
+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.
+
+\indexisarant{thm}\indexisarant{prop}\indexisarant{term}\indexisarant{typ}
+\begin{rail}
+  atsign lbrace antiquotation rbrace
+  ;
+
+  antiquotation:
+    'thm' options thmrefs |
+    'prop' options prop |
+    'term' options term |
+    'typ' options type
+  ;
+  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|*}|.
+
+\medskip
+
+The following options are available to tune the output.
+\begin{descr}
+\item[$show_types = bool$ and $show_sorts = bool$] refer to Isabelle's global
+  ML flags of the same names (see also \cite{isabelle-ref}).
+\item[$display = bool$] indicates if the text is to be output as multi-line
+  ``display material'', rather than a small piece of text without line breaks
+  (which is the default).
+\item[$quotes = bool$] indicates if the output should be enclosed in double
+  quotes.
+\item[$mode = name$] adds $name$ to the print mode to be used for
+  presentation.  Note that the standard setup for {\LaTeX} output is already
+  present by default, including the modes ``$latex$'', ``$xsymbols$'',
+  ``$symbols$''.
+\item[$margin = nat$] changes the margin for pretty printing of display
+  material.
+\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.
+
+
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "isar-ref"