doc-src/IsarRef/Thy/document/Document_Preparation.tex
changeset 27042 8fcf19f2168b
child 27052 5c48cecb981b
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Mon Jun 02 22:50:29 2008 +0200
     1.3 @@ -0,0 +1,454 @@
     1.4 +%
     1.5 +\begin{isabellebody}%
     1.6 +\def\isabellecontext{Document{\isacharunderscore}Preparation}%
     1.7 +%
     1.8 +\isadelimtheory
     1.9 +\isanewline
    1.10 +\isanewline
    1.11 +%
    1.12 +\endisadelimtheory
    1.13 +%
    1.14 +\isatagtheory
    1.15 +\isacommand{theory}\isamarkupfalse%
    1.16 +\ Document{\isacharunderscore}Preparation\isanewline
    1.17 +\isakeyword{imports}\ Main\isanewline
    1.18 +\isakeyword{begin}%
    1.19 +\endisatagtheory
    1.20 +{\isafoldtheory}%
    1.21 +%
    1.22 +\isadelimtheory
    1.23 +%
    1.24 +\endisadelimtheory
    1.25 +%
    1.26 +\isamarkupchapter{Document preparation \label{ch:document-prep}%
    1.27 +}
    1.28 +\isamarkuptrue%
    1.29 +%
    1.30 +\begin{isamarkuptext}%
    1.31 +Isabelle/Isar provides a simple document preparation system based on
    1.32 +  existing {PDF-\LaTeX} technology, with full support of hyper-links
    1.33 +  (both local references and URLs) and bookmarks.  Thus the results
    1.34 +  are equally well suited for WWW browsing and as printed copies.
    1.35 +
    1.36 +  \medskip Isabelle generates {\LaTeX} output as part of the run of a
    1.37 +  \emph{logic session} (see also \cite{isabelle-sys}).  Getting
    1.38 +  started with a working configuration for common situations is quite
    1.39 +  easy by using the Isabelle \verb|mkdir| and \verb|make|
    1.40 +  tools.  First invoke
    1.41 +\begin{ttbox}
    1.42 +  isatool mkdir Foo
    1.43 +\end{ttbox}
    1.44 +  to initialize a separate directory for session \verb|Foo| ---
    1.45 +  it is safe to experiment, since \verb|isatool mkdir| never
    1.46 +  overwrites existing files.  Ensure that \verb|Foo/ROOT.ML|
    1.47 +  holds ML commands to load all theories required for this session;
    1.48 +  furthermore \verb|Foo/document/root.tex| should include any
    1.49 +  special {\LaTeX} macro packages required for your document (the
    1.50 +  default is usually sufficient as a start).
    1.51 +
    1.52 +  The session is controlled by a separate \verb|IsaMakefile|
    1.53 +  (with crude source dependencies by default).  This file is located
    1.54 +  one level up from the \verb|Foo| directory location.  Now
    1.55 +  invoke
    1.56 +\begin{ttbox}
    1.57 +  isatool make Foo
    1.58 +\end{ttbox}
    1.59 +  to run the \verb|Foo| session, with browser information and
    1.60 +  document preparation enabled.  Unless any errors are reported by
    1.61 +  Isabelle or {\LaTeX}, the output will appear inside the directory
    1.62 +  \verb|ISABELLE_BROWSER_INFO|, as reported by the batch job in
    1.63 +  verbose mode.
    1.64 +
    1.65 +  \medskip You may also consider to tune the \verb|usedir|
    1.66 +  options in \verb|IsaMakefile|, for example to change the output
    1.67 +  format from \verb|pdf| to \verb|dvi|, or activate the
    1.68 +  \verb|-D| option to retain a second copy of the generated
    1.69 +  {\LaTeX} sources.
    1.70 +
    1.71 +  \medskip See \emph{The Isabelle System Manual} \cite{isabelle-sys}
    1.72 +  for further details on Isabelle logic sessions and theory
    1.73 +  presentation.  The Isabelle/HOL tutorial \cite{isabelle-hol-book}
    1.74 +  also covers theory presentation issues.%
    1.75 +\end{isamarkuptext}%
    1.76 +\isamarkuptrue%
    1.77 +%
    1.78 +\isamarkupsection{Markup commands \label{sec:markup}%
    1.79 +}
    1.80 +\isamarkuptrue%
    1.81 +%
    1.82 +\begin{isamarkuptext}%
    1.83 +\begin{matharray}{rcl}
    1.84 +    \indexdef{}{command}{chapter}\hypertarget{command.chapter}{\hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}} & : & \isarkeep{local{\dsh}theory} \\
    1.85 +    \indexdef{}{command}{section}\hypertarget{command.section}{\hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}}} & : & \isarkeep{local{\dsh}theory} \\
    1.86 +    \indexdef{}{command}{subsection}\hypertarget{command.subsection}{\hyperlink{command.subsection}{\mbox{\isa{\isacommand{subsection}}}}} & : & \isarkeep{local{\dsh}theory} \\
    1.87 +    \indexdef{}{command}{subsubsection}\hypertarget{command.subsubsection}{\hyperlink{command.subsubsection}{\mbox{\isa{\isacommand{subsubsection}}}}} & : & \isarkeep{local{\dsh}theory} \\
    1.88 +    \indexdef{}{command}{text}\hypertarget{command.text}{\hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}}} & : & \isarkeep{local{\dsh}theory} \\
    1.89 +    \indexdef{}{command}{text\_raw}\hypertarget{command.text-raw}{\hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}} & : & \isarkeep{local{\dsh}theory} \\[0.5ex]
    1.90 +    \indexdef{}{command}{sect}\hypertarget{command.sect}{\hyperlink{command.sect}{\mbox{\isa{\isacommand{sect}}}}} & : & \isartrans{proof}{proof} \\
    1.91 +    \indexdef{}{command}{subsect}\hypertarget{command.subsect}{\hyperlink{command.subsect}{\mbox{\isa{\isacommand{subsect}}}}} & : & \isartrans{proof}{proof} \\
    1.92 +    \indexdef{}{command}{subsubsect}\hypertarget{command.subsubsect}{\hyperlink{command.subsubsect}{\mbox{\isa{\isacommand{subsubsect}}}}} & : & \isartrans{proof}{proof} \\
    1.93 +    \indexdef{}{command}{txt}\hypertarget{command.txt}{\hyperlink{command.txt}{\mbox{\isa{\isacommand{txt}}}}} & : & \isartrans{proof}{proof} \\
    1.94 +    \indexdef{}{command}{txt\_raw}\hypertarget{command.txt-raw}{\hyperlink{command.txt-raw}{\mbox{\isa{\isacommand{txt{\isacharunderscore}raw}}}}} & : & \isartrans{proof}{proof} \\
    1.95 +  \end{matharray}
    1.96 +
    1.97 +  Apart from formal comments (see \secref{sec:comments}), markup
    1.98 +  commands provide a structured way to insert text into the document
    1.99 +  generated from a theory (see \cite{isabelle-sys} for more
   1.100 +  information on Isabelle's document preparation tools).
   1.101 +
   1.102 +  \begin{rail}
   1.103 +    ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
   1.104 +    ;
   1.105 +    ('text\_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
   1.106 +    ;
   1.107 +  \end{rail}
   1.108 +
   1.109 +  \begin{descr}
   1.110 +
   1.111 +  \item [\hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}, \hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}}, \hyperlink{command.subsection}{\mbox{\isa{\isacommand{subsection}}}}, and \hyperlink{command.subsubsection}{\mbox{\isa{\isacommand{subsubsection}}}}] mark chapter and
   1.112 +  section headings.
   1.113 +
   1.114 +  \item [\hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}} and \hyperlink{command.txt}{\mbox{\isa{\isacommand{txt}}}}] specify paragraphs of
   1.115 +  plain text.
   1.116 +
   1.117 +  \item [\hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}} and \hyperlink{command.txt-raw}{\mbox{\isa{\isacommand{txt{\isacharunderscore}raw}}}}] insert
   1.118 +  {\LaTeX} source into the output, without additional markup.  Thus
   1.119 +  the full range of document manipulations becomes available.
   1.120 +
   1.121 +  \end{descr}
   1.122 +
   1.123 +  The \isa{{\isachardoublequote}text{\isachardoublequote}} argument of these markup commands (except for
   1.124 +  \hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}) may contain references to formal entities
   1.125 +  (``antiquotations'', see also \secref{sec:antiq}).  These are
   1.126 +  interpreted in the present theory context, or the named \isa{{\isachardoublequote}target{\isachardoublequote}}.
   1.127 +
   1.128 +  Any of these markup elements corresponds to a {\LaTeX} command with
   1.129 +  the name prefixed by \verb|\isamarkup|.  For the sectioning
   1.130 +  commands this is a plain macro with a single argument, e.g.\
   1.131 +  \verb|\isamarkupchapter{|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|}| for
   1.132 +  \hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}.  The \hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}} markup results in a
   1.133 +  {\LaTeX} environment \verb|\begin{isamarkuptext}| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|\end{isamarkuptext}|, while \hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}
   1.134 +  causes the text to be inserted directly into the {\LaTeX} source.
   1.135 +
   1.136 +  \medskip The proof markup commands closely resemble those for theory
   1.137 +  specifications, but have a different formal status and produce
   1.138 +  different {\LaTeX} macros.  Also note that the \indexref{}{command}{header}\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}} declaration (see \secref{sec:begin-thy}) admits to insert
   1.139 +  section markup just preceding the actual theory definition.%
   1.140 +\end{isamarkuptext}%
   1.141 +\isamarkuptrue%
   1.142 +%
   1.143 +\isamarkupsection{Antiquotations \label{sec:antiq}%
   1.144 +}
   1.145 +\isamarkuptrue%
   1.146 +%
   1.147 +\begin{isamarkuptext}%
   1.148 +\begin{matharray}{rcl}
   1.149 +    \indexdef{}{antiquotation}{theory}\hypertarget{antiquotation.theory}{\hyperlink{antiquotation.theory}{\mbox{\isa{theory}}}} & : & \isarantiq \\
   1.150 +    \indexdef{}{antiquotation}{thm}\hypertarget{antiquotation.thm}{\hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}} & : & \isarantiq \\
   1.151 +    \indexdef{}{antiquotation}{prop}\hypertarget{antiquotation.prop}{\hyperlink{antiquotation.prop}{\mbox{\isa{prop}}}} & : & \isarantiq \\
   1.152 +    \indexdef{}{antiquotation}{term}\hypertarget{antiquotation.term}{\hyperlink{antiquotation.term}{\mbox{\isa{term}}}} & : & \isarantiq \\
   1.153 +    \indexdef{}{antiquotation}{const}\hypertarget{antiquotation.const}{\hyperlink{antiquotation.const}{\mbox{\isa{const}}}} & : & \isarantiq \\
   1.154 +    \indexdef{}{antiquotation}{abbrev}\hypertarget{antiquotation.abbrev}{\hyperlink{antiquotation.abbrev}{\mbox{\isa{abbrev}}}} & : & \isarantiq \\
   1.155 +    \indexdef{}{antiquotation}{typeof}\hypertarget{antiquotation.typeof}{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}} & : & \isarantiq \\
   1.156 +    \indexdef{}{antiquotation}{typ}\hypertarget{antiquotation.typ}{\hyperlink{antiquotation.typ}{\mbox{\isa{typ}}}} & : & \isarantiq \\
   1.157 +    \indexdef{}{antiquotation}{thm\_style}\hypertarget{antiquotation.thm-style}{\hyperlink{antiquotation.thm-style}{\mbox{\isa{thm{\isacharunderscore}style}}}} & : & \isarantiq \\
   1.158 +    \indexdef{}{antiquotation}{term\_style}\hypertarget{antiquotation.term-style}{\hyperlink{antiquotation.term-style}{\mbox{\isa{term{\isacharunderscore}style}}}} & : & \isarantiq \\
   1.159 +    \indexdef{}{antiquotation}{text}\hypertarget{antiquotation.text}{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}} & : & \isarantiq \\
   1.160 +    \indexdef{}{antiquotation}{goals}\hypertarget{antiquotation.goals}{\hyperlink{antiquotation.goals}{\mbox{\isa{goals}}}} & : & \isarantiq \\
   1.161 +    \indexdef{}{antiquotation}{subgoals}\hypertarget{antiquotation.subgoals}{\hyperlink{antiquotation.subgoals}{\mbox{\isa{subgoals}}}} & : & \isarantiq \\
   1.162 +    \indexdef{}{antiquotation}{prf}\hypertarget{antiquotation.prf}{\hyperlink{antiquotation.prf}{\mbox{\isa{prf}}}} & : & \isarantiq \\
   1.163 +    \indexdef{}{antiquotation}{full\_prf}\hypertarget{antiquotation.full-prf}{\hyperlink{antiquotation.full-prf}{\mbox{\isa{full{\isacharunderscore}prf}}}} & : & \isarantiq \\
   1.164 +    \indexdef{}{antiquotation}{ML}\hypertarget{antiquotation.ML}{\hyperlink{antiquotation.ML}{\mbox{\isa{ML}}}} & : & \isarantiq \\
   1.165 +    \indexdef{}{antiquotation}{ML\_type}\hypertarget{antiquotation.ML-type}{\hyperlink{antiquotation.ML-type}{\mbox{\isa{ML{\isacharunderscore}type}}}} & : & \isarantiq \\
   1.166 +    \indexdef{}{antiquotation}{ML\_struct}\hypertarget{antiquotation.ML-struct}{\hyperlink{antiquotation.ML-struct}{\mbox{\isa{ML{\isacharunderscore}struct}}}} & : & \isarantiq \\
   1.167 +  \end{matharray}
   1.168 +
   1.169 +  The text body of formal comments (see also \secref{sec:comments})
   1.170 +  may contain antiquotations of logical entities, such as theorems,
   1.171 +  terms and types, which are to be presented in the final output
   1.172 +  produced by the Isabelle document preparation system (see also
   1.173 +  \chref{ch:document-prep}).
   1.174 +
   1.175 +  Thus embedding of ``\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ {\isacharbrackleft}show{\isacharunderscore}types{\isacharbrackright}\ {\isachardoublequote}f\ x\ {\isacharequal}\ a\ {\isacharplus}\ x{\isachardoublequote}{\isacharbraceright}{\isachardoublequote}}''
   1.176 +  within a text block would cause
   1.177 +  \isa{{\isacharparenleft}f{\isasymColon}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharplus}\ x} to appear in the final {\LaTeX} document.  Also note that theorem
   1.178 +  antiquotations may involve attributes as well.  For example,
   1.179 +  \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm\ sym\ {\isacharbrackleft}no{\isacharunderscore}vars{\isacharbrackright}{\isacharbraceright}{\isachardoublequote}} would print the theorem's
   1.180 +  statement where all schematic variables have been replaced by fixed
   1.181 +  ones, which are easier to read.
   1.182 +
   1.183 +  \begin{rail}
   1.184 +    atsign lbrace antiquotation rbrace
   1.185 +    ;
   1.186 +
   1.187 +    antiquotation:
   1.188 +      'theory' options name |
   1.189 +      'thm' options thmrefs |
   1.190 +      'prop' options prop |
   1.191 +      'term' options term |
   1.192 +      'const' options term |
   1.193 +      'abbrev' options term |
   1.194 +      'typeof' options term |
   1.195 +      'typ' options type |
   1.196 +      'thm\_style' options name thmref |
   1.197 +      'term\_style' options name term |
   1.198 +      'text' options name |
   1.199 +      'goals' options |
   1.200 +      'subgoals' options |
   1.201 +      'prf' options thmrefs |
   1.202 +      'full\_prf' options thmrefs |
   1.203 +      'ML' options name |
   1.204 +      'ML\_type' options name |
   1.205 +      'ML\_struct' options name
   1.206 +    ;
   1.207 +    options: '[' (option * ',') ']'
   1.208 +    ;
   1.209 +    option: name | name '=' name
   1.210 +    ;
   1.211 +  \end{rail}
   1.212 +
   1.213 +  Note that the syntax of antiquotations may \emph{not} include source
   1.214 +  comments \verb|(*|~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\verb|*)| or verbatim
   1.215 +  text \verb|{|\verb|*|~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\verb|*|\verb|}|.
   1.216 +
   1.217 +  \begin{descr}
   1.218 +  
   1.219 +  \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}theory\ A{\isacharbraceright}{\isachardoublequote}}] prints the name \isa{{\isachardoublequote}A{\isachardoublequote}}, which is
   1.220 +  guaranteed to refer to a valid ancestor theory in the current
   1.221 +  context.
   1.222 +
   1.223 +  \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] prints theorems
   1.224 +  \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}.  Note that attribute specifications
   1.225 +  may be included as well (see also \secref{sec:syn-att}); the
   1.226 +  \indexref{}{attribute}{no\_vars}\hyperlink{attribute.no-vars}{\mbox{\isa{no{\isacharunderscore}vars}}} rule (see \secref{sec:misc-meth-att}) would
   1.227 +  be particularly useful to suppress printing of schematic variables.
   1.228 +
   1.229 +  \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prop\ {\isasymphi}{\isacharbraceright}{\isachardoublequote}}] prints a well-typed proposition \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}.
   1.230 +
   1.231 +  \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ t{\isacharbraceright}{\isachardoublequote}}] prints a well-typed term \isa{{\isachardoublequote}t{\isachardoublequote}}.
   1.232 +
   1.233 +  \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}const\ c{\isacharbraceright}{\isachardoublequote}}] prints a logical or syntactic constant
   1.234 +  \isa{{\isachardoublequote}c{\isachardoublequote}}.
   1.235 +  
   1.236 +  \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}abbrev\ c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] prints a constant
   1.237 +  abbreviation \isa{{\isachardoublequote}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ rhs{\isachardoublequote}} as defined in
   1.238 +  the current context.
   1.239 +
   1.240 +  \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typeof\ t{\isacharbraceright}{\isachardoublequote}}] prints the type of a well-typed term
   1.241 +  \isa{{\isachardoublequote}t{\isachardoublequote}}.
   1.242 +
   1.243 +  \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typ\ {\isasymtau}{\isacharbraceright}{\isachardoublequote}}] prints a well-formed type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}.
   1.244 +  
   1.245 +  \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm{\isacharunderscore}style\ s\ a{\isacharbraceright}{\isachardoublequote}}] prints theorem \isa{a},
   1.246 +  previously applying a style \isa{s} to it (see below).
   1.247 +  
   1.248 +  \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term{\isacharunderscore}style\ s\ t{\isacharbraceright}{\isachardoublequote}}] prints a well-typed term \isa{t} after applying a style \isa{s} to it (see below).
   1.249 +
   1.250 +  \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}text\ s{\isacharbraceright}{\isachardoublequote}}] prints uninterpreted source text \isa{s}.  This is particularly useful to print portions of text according
   1.251 +  to the Isabelle {\LaTeX} output style, without demanding
   1.252 +  well-formedness (e.g.\ small pieces of terms that should not be
   1.253 +  parsed or type-checked yet).
   1.254 +
   1.255 +  \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}goals{\isacharbraceright}{\isachardoublequote}}] prints the current \emph{dynamic} goal
   1.256 +  state.  This is mainly for support of tactic-emulation scripts
   1.257 +  within Isar --- presentation of goal states does not conform to
   1.258 +  actual human-readable proof documents.
   1.259 +
   1.260 +  Please do not include goal states into document output unless you
   1.261 +  really know what you are doing!
   1.262 +  
   1.263 +  \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}subgoals{\isacharbraceright}{\isachardoublequote}}] is similar to \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}goals{\isacharbraceright}{\isachardoublequote}}, but
   1.264 +  does not print the main goal.
   1.265 +  
   1.266 +  \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] prints the (compact)
   1.267 +  proof terms corresponding to the theorems \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}. Note that this requires proof terms to be switched on
   1.268 +  for the current object logic (see the ``Proof terms'' section of the
   1.269 +  Isabelle reference manual for information on how to do this).
   1.270 +  
   1.271 +  \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}full{\isacharunderscore}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] is like \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}, but displays the full proof terms,
   1.272 +  i.e.\ also displays information omitted in the compact proof term,
   1.273 +  which is denoted by ``\isa{{\isacharunderscore}}'' placeholders there.
   1.274 +  
   1.275 +  \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}ML\ s{\isacharbraceright}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}ML{\isacharunderscore}type\ s{\isacharbraceright}{\isachardoublequote}}, and \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}ML{\isacharunderscore}struct\ s{\isacharbraceright}{\isachardoublequote}}] check text \isa{s} as ML value, type, and
   1.276 +  structure, respectively.  The source is displayed verbatim.
   1.277 +
   1.278 +  \end{descr}
   1.279 +
   1.280 +  \medskip The following standard styles for use with \isa{thm{\isacharunderscore}style} and \isa{term{\isacharunderscore}style} are available:
   1.281 +
   1.282 +  \begin{descr}
   1.283 +  
   1.284 +  \item [\isa{lhs}] extracts the first argument of any application
   1.285 +  form with at least two arguments -- typically meta-level or
   1.286 +  object-level equality, or any other binary relation.
   1.287 +  
   1.288 +  \item [\isa{rhs}] is like \isa{lhs}, but extracts the second
   1.289 +  argument.
   1.290 +  
   1.291 +  \item [\isa{{\isachardoublequote}concl{\isachardoublequote}}] extracts the conclusion \isa{C} from a rule
   1.292 +  in Horn-clause normal form \isa{{\isachardoublequote}A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C{\isachardoublequote}}.
   1.293 +  
   1.294 +  \item [\isa{{\isachardoublequote}prem{\isadigit{1}}{\isachardoublequote}}, \dots, \isa{{\isachardoublequote}prem{\isadigit{9}}{\isachardoublequote}}] extract premise
   1.295 +  number \isa{{\isachardoublequote}{\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isadigit{9}}{\isachardoublequote}}, respectively, from from a rule in
   1.296 +  Horn-clause normal form \isa{{\isachardoublequote}A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C{\isachardoublequote}}
   1.297 +
   1.298 +  \end{descr}
   1.299 +
   1.300 +  \medskip
   1.301 +  The following options are available to tune the output.  Note that most of
   1.302 +  these coincide with ML flags of the same names (see also \cite{isabelle-ref}).
   1.303 +
   1.304 +  \begin{descr}
   1.305 +
   1.306 +  \item[\isa{{\isachardoublequote}show{\isacharunderscore}types\ {\isacharequal}\ bool{\isachardoublequote}} and \isa{{\isachardoublequote}show{\isacharunderscore}sorts\ {\isacharequal}\ bool{\isachardoublequote}}]
   1.307 +  control printing of explicit type and sort constraints.
   1.308 +
   1.309 +  \item[\isa{{\isachardoublequote}show{\isacharunderscore}structs\ {\isacharequal}\ bool{\isachardoublequote}}] controls printing of implicit
   1.310 +  structures.
   1.311 +
   1.312 +  \item[\isa{{\isachardoublequote}long{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}}] forces names of types and
   1.313 +  constants etc.\ to be printed in their fully qualified internal
   1.314 +  form.
   1.315 +
   1.316 +  \item[\isa{{\isachardoublequote}short{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}}] forces names of types and
   1.317 +  constants etc.\ to be printed unqualified.  Note that internalizing
   1.318 +  the output again in the current context may well yield a different
   1.319 +  result.
   1.320 +
   1.321 +  \item[\isa{{\isachardoublequote}unique{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}}] determines whether the printed
   1.322 +  version of qualified names should be made sufficiently long to avoid
   1.323 +  overlap with names declared further back.  Set to \isa{false} for
   1.324 +  more concise output.
   1.325 +
   1.326 +  \item[\isa{{\isachardoublequote}eta{\isacharunderscore}contract\ {\isacharequal}\ bool{\isachardoublequote}}] prints terms in \isa{{\isasymeta}}-contracted form.
   1.327 +
   1.328 +  \item[\isa{{\isachardoublequote}display\ {\isacharequal}\ bool{\isachardoublequote}}] indicates if the text is to be
   1.329 +  output as multi-line ``display material'', rather than a small piece
   1.330 +  of text without line breaks (which is the default).
   1.331 +
   1.332 +  \item[\isa{{\isachardoublequote}break\ {\isacharequal}\ bool{\isachardoublequote}}] controls line breaks in non-display
   1.333 +  material.
   1.334 +
   1.335 +  \item[\isa{{\isachardoublequote}quotes\ {\isacharequal}\ bool{\isachardoublequote}}] indicates if the output should be
   1.336 +  enclosed in double quotes.
   1.337 +
   1.338 +  \item[\isa{{\isachardoublequote}mode\ {\isacharequal}\ name{\isachardoublequote}}] adds \isa{name} to the print mode to
   1.339 +  be used for presentation (see also \cite{isabelle-ref}).  Note that
   1.340 +  the standard setup for {\LaTeX} output is already present by
   1.341 +  default, including the modes \isa{latex} and \isa{xsymbols}.
   1.342 +
   1.343 +  \item[\isa{{\isachardoublequote}margin\ {\isacharequal}\ nat{\isachardoublequote}} and \isa{{\isachardoublequote}indent\ {\isacharequal}\ nat{\isachardoublequote}}] change the
   1.344 +  margin or indentation for pretty printing of display material.
   1.345 +
   1.346 +  \item[\isa{{\isachardoublequote}source\ {\isacharequal}\ bool{\isachardoublequote}}] prints the source text of the
   1.347 +  antiquotation arguments, rather than the actual value.  Note that
   1.348 +  this does not affect well-formedness checks of \hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}, \hyperlink{antiquotation.term}{\mbox{\isa{term}}}, etc. (only the \hyperlink{antiquotation.text}{\mbox{\isa{text}}} antiquotation admits arbitrary output).
   1.349 +
   1.350 +  \item[\isa{{\isachardoublequote}goals{\isacharunderscore}limit\ {\isacharequal}\ nat{\isachardoublequote}}] determines the maximum number of
   1.351 +  goals to be printed.
   1.352 +
   1.353 +  \item[\isa{{\isachardoublequote}locale\ {\isacharequal}\ name{\isachardoublequote}}] specifies an alternative locale
   1.354 +  context used for evaluating and printing the subsequent argument.
   1.355 +
   1.356 +  \end{descr}
   1.357 +
   1.358 +  For boolean flags, ``\isa{{\isachardoublequote}name\ {\isacharequal}\ true{\isachardoublequote}}'' may be abbreviated as
   1.359 +  ``\isa{name}''.  All of the above flags are disabled by default,
   1.360 +  unless changed from ML.
   1.361 +
   1.362 +  \medskip Note that antiquotations do not only spare the author from
   1.363 +  tedious typing of logical entities, but also achieve some degree of
   1.364 +  consistency-checking of informal explanations with formal
   1.365 +  developments: well-formedness of terms and types with respect to the
   1.366 +  current theory or proof context is ensured here.%
   1.367 +\end{isamarkuptext}%
   1.368 +\isamarkuptrue%
   1.369 +%
   1.370 +\isamarkupsection{Tagged commands \label{sec:tags}%
   1.371 +}
   1.372 +\isamarkuptrue%
   1.373 +%
   1.374 +\begin{isamarkuptext}%
   1.375 +Each Isabelle/Isar command may be decorated by presentation tags:
   1.376 +
   1.377 +  \indexouternonterm{tags}
   1.378 +  \begin{rail}
   1.379 +    tags: ( tag * )
   1.380 +    ;
   1.381 +    tag: '\%' (ident | string)
   1.382 +  \end{rail}
   1.383 +
   1.384 +  The tags \isa{{\isachardoublequote}theory{\isachardoublequote}}, \isa{{\isachardoublequote}proof{\isachardoublequote}}, \isa{{\isachardoublequote}ML{\isachardoublequote}} are already
   1.385 +  pre-declared for certain classes of commands:
   1.386 +
   1.387 + \medskip
   1.388 +
   1.389 +  \begin{tabular}{ll}
   1.390 +    \isa{{\isachardoublequote}theory{\isachardoublequote}} & theory begin/end \\
   1.391 +    \isa{{\isachardoublequote}proof{\isachardoublequote}} & all proof commands \\
   1.392 +    \isa{{\isachardoublequote}ML{\isachardoublequote}} & all commands involving ML code \\
   1.393 +  \end{tabular}
   1.394 +
   1.395 +  \medskip The Isabelle document preparation system (see also
   1.396 +  \cite{isabelle-sys}) allows tagged command regions to be presented
   1.397 +  specifically, e.g.\ to fold proof texts, or drop parts of the text
   1.398 +  completely.
   1.399 +
   1.400 +  For example ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharpercent}invisible\ auto{\isachardoublequote}}'' would
   1.401 +  cause that piece of proof to be treated as \isa{invisible} instead
   1.402 +  of \isa{{\isachardoublequote}proof{\isachardoublequote}} (the default), which may be either show or hidden
   1.403 +  depending on the document setup.  In contrast, ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharpercent}visible\ auto{\isachardoublequote}}'' would force this text to be shown
   1.404 +  invariably.
   1.405 +
   1.406 +  Explicit tag specifications within a proof apply to all subsequent
   1.407 +  commands of the same level of nesting.  For example, ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}{\isacharpercent}visible\ {\isasymdots}{\isachardoublequote}}~\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}'' would force the
   1.408 +  whole sub-proof to be typeset as \isa{visible} (unless some of its
   1.409 +  parts are tagged differently).%
   1.410 +\end{isamarkuptext}%
   1.411 +\isamarkuptrue%
   1.412 +%
   1.413 +\isamarkupsection{Draft presentation%
   1.414 +}
   1.415 +\isamarkuptrue%
   1.416 +%
   1.417 +\begin{isamarkuptext}%
   1.418 +\begin{matharray}{rcl}
   1.419 +    \indexdef{}{command}{display\_drafts}\hypertarget{command.display-drafts}{\hyperlink{command.display-drafts}{\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
   1.420 +    \indexdef{}{command}{print\_drafts}\hypertarget{command.print-drafts}{\hyperlink{command.print-drafts}{\mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
   1.421 +  \end{matharray}
   1.422 +
   1.423 +  \begin{rail}
   1.424 +    ('display\_drafts' | 'print\_drafts') (name +)
   1.425 +    ;
   1.426 +  \end{rail}
   1.427 +
   1.428 +  \begin{descr}
   1.429 +
   1.430 +  \item [\hyperlink{command.display-drafts}{\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}}~\isa{paths} and \hyperlink{command.print-drafts}{\mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}}~\isa{paths}] perform simple output of a given list
   1.431 +  of raw source files.  Only those symbols that do not require
   1.432 +  additional {\LaTeX} packages are displayed properly, everything else
   1.433 +  is left verbatim.
   1.434 +
   1.435 +  \end{descr}%
   1.436 +\end{isamarkuptext}%
   1.437 +\isamarkuptrue%
   1.438 +%
   1.439 +\isadelimtheory
   1.440 +%
   1.441 +\endisadelimtheory
   1.442 +%
   1.443 +\isatagtheory
   1.444 +\isacommand{end}\isamarkupfalse%
   1.445 +%
   1.446 +\endisatagtheory
   1.447 +{\isafoldtheory}%
   1.448 +%
   1.449 +\isadelimtheory
   1.450 +%
   1.451 +\endisadelimtheory
   1.452 +\isanewline
   1.453 +\end{isabellebody}%
   1.454 +%%% Local Variables:
   1.455 +%%% mode: latex
   1.456 +%%% TeX-master: "root"
   1.457 +%%% End: