# 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