doc-src/IsarRef/Thy/document/Document_Preparation.tex
author wenzelm
Sat Oct 04 17:40:58 2008 +0200 (2008-10-04)
changeset 28505 f98751bd715f
parent 27881 f0d543629376
child 28788 ff9d8a8932e4
permissions -rw-r--r--
updated generated file;
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Document{\isacharunderscore}Preparation}%
     4 %
     5 \isadelimtheory
     6 \isanewline
     7 \isanewline
     8 %
     9 \endisadelimtheory
    10 %
    11 \isatagtheory
    12 \isacommand{theory}\isamarkupfalse%
    13 \ Document{\isacharunderscore}Preparation\isanewline
    14 \isakeyword{imports}\ Main\isanewline
    15 \isakeyword{begin}%
    16 \endisatagtheory
    17 {\isafoldtheory}%
    18 %
    19 \isadelimtheory
    20 %
    21 \endisadelimtheory
    22 %
    23 \isamarkupchapter{Document preparation \label{ch:document-prep}%
    24 }
    25 \isamarkuptrue%
    26 %
    27 \begin{isamarkuptext}%
    28 Isabelle/Isar provides a simple document preparation system based on
    29   existing {PDF-\LaTeX} technology, with full support of hyper-links
    30   (both local references and URLs) and bookmarks.  Thus the results
    31   are equally well suited for WWW browsing and as printed copies.
    32 
    33   \medskip Isabelle generates {\LaTeX} output as part of the run of a
    34   \emph{logic session} (see also \cite{isabelle-sys}).  Getting
    35   started with a working configuration for common situations is quite
    36   easy by using the Isabelle \verb|mkdir| and \verb|make|
    37   tools.  First invoke
    38 \begin{ttbox}
    39   isabelle mkdir Foo
    40 \end{ttbox}
    41   to initialize a separate directory for session \verb|Foo| ---
    42   it is safe to experiment, since \verb|isabelle mkdir| never
    43   overwrites existing files.  Ensure that \verb|Foo/ROOT.ML|
    44   holds ML commands to load all theories required for this session;
    45   furthermore \verb|Foo/document/root.tex| should include any
    46   special {\LaTeX} macro packages required for your document (the
    47   default is usually sufficient as a start).
    48 
    49   The session is controlled by a separate \verb|IsaMakefile|
    50   (with crude source dependencies by default).  This file is located
    51   one level up from the \verb|Foo| directory location.  Now
    52   invoke
    53 \begin{ttbox}
    54   isabelle make Foo
    55 \end{ttbox}
    56   to run the \verb|Foo| session, with browser information and
    57   document preparation enabled.  Unless any errors are reported by
    58   Isabelle or {\LaTeX}, the output will appear inside the directory
    59   \verb|ISABELLE_BROWSER_INFO|, as reported by the batch job in
    60   verbose mode.
    61 
    62   \medskip You may also consider to tune the \verb|usedir|
    63   options in \verb|IsaMakefile|, for example to change the output
    64   format from \verb|pdf| to \verb|dvi|, or activate the
    65   \verb|-D| option to retain a second copy of the generated
    66   {\LaTeX} sources.
    67 
    68   \medskip See \emph{The Isabelle System Manual} \cite{isabelle-sys}
    69   for further details on Isabelle logic sessions and theory
    70   presentation.  The Isabelle/HOL tutorial \cite{isabelle-hol-book}
    71   also covers theory presentation issues.%
    72 \end{isamarkuptext}%
    73 \isamarkuptrue%
    74 %
    75 \isamarkupsection{Markup commands \label{sec:markup}%
    76 }
    77 \isamarkuptrue%
    78 %
    79 \begin{isamarkuptext}%
    80 \begin{matharray}{rcl}
    81     \indexdef{}{command}{header}\hypertarget{command.header}{\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}}} & : & \isarkeep{toplevel} \\[0.5ex]
    82     \indexdef{}{command}{chapter}\hypertarget{command.chapter}{\hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}} & : & \isarkeep{local{\dsh}theory} \\
    83     \indexdef{}{command}{section}\hypertarget{command.section}{\hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}}} & : & \isarkeep{local{\dsh}theory} \\
    84     \indexdef{}{command}{subsection}\hypertarget{command.subsection}{\hyperlink{command.subsection}{\mbox{\isa{\isacommand{subsection}}}}} & : & \isarkeep{local{\dsh}theory} \\
    85     \indexdef{}{command}{subsubsection}\hypertarget{command.subsubsection}{\hyperlink{command.subsubsection}{\mbox{\isa{\isacommand{subsubsection}}}}} & : & \isarkeep{local{\dsh}theory} \\
    86     \indexdef{}{command}{text}\hypertarget{command.text}{\hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}}} & : & \isarkeep{local{\dsh}theory} \\
    87     \indexdef{}{command}{text\_raw}\hypertarget{command.text-raw}{\hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}} & : & \isarkeep{local{\dsh}theory} \\[0.5ex]
    88     \indexdef{}{command}{sect}\hypertarget{command.sect}{\hyperlink{command.sect}{\mbox{\isa{\isacommand{sect}}}}} & : & \isartrans{proof}{proof} \\
    89     \indexdef{}{command}{subsect}\hypertarget{command.subsect}{\hyperlink{command.subsect}{\mbox{\isa{\isacommand{subsect}}}}} & : & \isartrans{proof}{proof} \\
    90     \indexdef{}{command}{subsubsect}\hypertarget{command.subsubsect}{\hyperlink{command.subsubsect}{\mbox{\isa{\isacommand{subsubsect}}}}} & : & \isartrans{proof}{proof} \\
    91     \indexdef{}{command}{txt}\hypertarget{command.txt}{\hyperlink{command.txt}{\mbox{\isa{\isacommand{txt}}}}} & : & \isartrans{proof}{proof} \\
    92     \indexdef{}{command}{txt\_raw}\hypertarget{command.txt-raw}{\hyperlink{command.txt-raw}{\mbox{\isa{\isacommand{txt{\isacharunderscore}raw}}}}} & : & \isartrans{proof}{proof} \\
    93   \end{matharray}
    94 
    95   Apart from formal comments (see \secref{sec:comments}), markup
    96   commands provide a structured way to insert text into the document
    97   generated from a theory (see \cite{isabelle-sys} for more
    98   information on Isabelle's document preparation tools).
    99 
   100   \begin{rail}
   101     ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
   102     ;
   103     ('header' | 'text\_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
   104     ;
   105   \end{rail}
   106 
   107   \begin{descr}
   108 
   109   \item [\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] provides plain text
   110   markup just preceding the formal beginning of a theory.  In actual
   111   document preparation the corresponding {\LaTeX} macro \verb|\isamarkupheader| may be redefined to produce chapter or section
   112   headings.
   113   
   114   \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
   115   section headings.  The corresponding {\LaTeX} macros are \verb|\isamarkupchapter|, \verb|\isamarkupsection| etc.
   116 
   117   \item [\hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}} and \hyperlink{command.txt}{\mbox{\isa{\isacommand{txt}}}}] specify paragraphs of
   118   plain text.
   119 
   120   \item [\hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}} and \hyperlink{command.txt-raw}{\mbox{\isa{\isacommand{txt{\isacharunderscore}raw}}}}] insert
   121   {\LaTeX} source into the output, without additional markup.  Thus
   122   the full range of document manipulations becomes available.
   123 
   124   \end{descr}
   125 
   126   The \isa{{\isachardoublequote}text{\isachardoublequote}} argument of these markup commands (except for
   127   \hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}) may contain references to formal entities
   128   (``antiquotations'', see also \secref{sec:antiq}).  These are
   129   interpreted in the present theory context, or the named \isa{{\isachardoublequote}target{\isachardoublequote}}.
   130 
   131   Any of these markup elements corresponds to a {\LaTeX} command with
   132   the name prefixed by \verb|\isamarkup|.  For the sectioning
   133   commands this is a plain macro with a single argument, e.g.\
   134   \verb|\isamarkupchapter{|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|}| for
   135   \hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}.  The \hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}} markup results in a
   136   {\LaTeX} environment \verb|\begin{isamarkuptext}| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|\end{isamarkuptext}|, while \hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}
   137   causes the text to be inserted directly into the {\LaTeX} source.
   138 
   139   \medskip The proof markup commands closely resemble those for theory
   140   specifications, but have a different formal status and produce
   141   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
   142   section markup just preceding the actual theory definition.%
   143 \end{isamarkuptext}%
   144 \isamarkuptrue%
   145 %
   146 \isamarkupsection{Antiquotations \label{sec:antiq}%
   147 }
   148 \isamarkuptrue%
   149 %
   150 \begin{isamarkuptext}%
   151 \begin{matharray}{rcl}
   152     \indexdef{}{antiquotation}{theory}\hypertarget{antiquotation.theory}{\hyperlink{antiquotation.theory}{\mbox{\isa{theory}}}} & : & \isarantiq \\
   153     \indexdef{}{antiquotation}{thm}\hypertarget{antiquotation.thm}{\hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}} & : & \isarantiq \\
   154     \indexdef{}{antiquotation}{lemma}\hypertarget{antiquotation.lemma}{\hyperlink{antiquotation.lemma}{\mbox{\isa{lemma}}}} & : & \isarantiq \\
   155     \indexdef{}{antiquotation}{prop}\hypertarget{antiquotation.prop}{\hyperlink{antiquotation.prop}{\mbox{\isa{prop}}}} & : & \isarantiq \\
   156     \indexdef{}{antiquotation}{term}\hypertarget{antiquotation.term}{\hyperlink{antiquotation.term}{\mbox{\isa{term}}}} & : & \isarantiq \\
   157     \indexdef{}{antiquotation}{const}\hypertarget{antiquotation.const}{\hyperlink{antiquotation.const}{\mbox{\isa{const}}}} & : & \isarantiq \\
   158     \indexdef{}{antiquotation}{abbrev}\hypertarget{antiquotation.abbrev}{\hyperlink{antiquotation.abbrev}{\mbox{\isa{abbrev}}}} & : & \isarantiq \\
   159     \indexdef{}{antiquotation}{typeof}\hypertarget{antiquotation.typeof}{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}} & : & \isarantiq \\
   160     \indexdef{}{antiquotation}{typ}\hypertarget{antiquotation.typ}{\hyperlink{antiquotation.typ}{\mbox{\isa{typ}}}} & : & \isarantiq \\
   161     \indexdef{}{antiquotation}{thm\_style}\hypertarget{antiquotation.thm-style}{\hyperlink{antiquotation.thm-style}{\mbox{\isa{thm{\isacharunderscore}style}}}} & : & \isarantiq \\
   162     \indexdef{}{antiquotation}{term\_style}\hypertarget{antiquotation.term-style}{\hyperlink{antiquotation.term-style}{\mbox{\isa{term{\isacharunderscore}style}}}} & : & \isarantiq \\
   163     \indexdef{}{antiquotation}{text}\hypertarget{antiquotation.text}{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}} & : & \isarantiq \\
   164     \indexdef{}{antiquotation}{goals}\hypertarget{antiquotation.goals}{\hyperlink{antiquotation.goals}{\mbox{\isa{goals}}}} & : & \isarantiq \\
   165     \indexdef{}{antiquotation}{subgoals}\hypertarget{antiquotation.subgoals}{\hyperlink{antiquotation.subgoals}{\mbox{\isa{subgoals}}}} & : & \isarantiq \\
   166     \indexdef{}{antiquotation}{prf}\hypertarget{antiquotation.prf}{\hyperlink{antiquotation.prf}{\mbox{\isa{prf}}}} & : & \isarantiq \\
   167     \indexdef{}{antiquotation}{full\_prf}\hypertarget{antiquotation.full-prf}{\hyperlink{antiquotation.full-prf}{\mbox{\isa{full{\isacharunderscore}prf}}}} & : & \isarantiq \\
   168     \indexdef{}{antiquotation}{ML}\hypertarget{antiquotation.ML}{\hyperlink{antiquotation.ML}{\mbox{\isa{ML}}}} & : & \isarantiq \\
   169     \indexdef{}{antiquotation}{ML\_type}\hypertarget{antiquotation.ML-type}{\hyperlink{antiquotation.ML-type}{\mbox{\isa{ML{\isacharunderscore}type}}}} & : & \isarantiq \\
   170     \indexdef{}{antiquotation}{ML\_struct}\hypertarget{antiquotation.ML-struct}{\hyperlink{antiquotation.ML-struct}{\mbox{\isa{ML{\isacharunderscore}struct}}}} & : & \isarantiq \\
   171   \end{matharray}
   172 
   173   The text body of formal comments (see also \secref{sec:comments})
   174   may contain antiquotations of logical entities, such as theorems,
   175   terms and types, which are to be presented in the final output
   176   produced by the Isabelle document preparation system.
   177 
   178   Thus embedding of ``\isa{{\isacharat}{\isacharbraceleft}term\ {\isacharbrackleft}show{\isacharunderscore}types{\isacharbrackright}\ {\isachardoublequote}f\ x\ {\isacharequal}\ a\ {\isacharplus}\ x{\isachardoublequote}{\isacharbraceright}}''
   179   within a text block would cause
   180   \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
   181   antiquotations may involve attributes as well.  For example,
   182   \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm\ sym\ {\isacharbrackleft}no{\isacharunderscore}vars{\isacharbrackright}{\isacharbraceright}{\isachardoublequote}} would print the theorem's
   183   statement where all schematic variables have been replaced by fixed
   184   ones, which are easier to read.
   185 
   186   \begin{rail}
   187     atsign lbrace antiquotation rbrace
   188     ;
   189 
   190     antiquotation:
   191       'theory' options name |
   192       'thm' options thmrefs |
   193       'lemma' options prop 'by' method |
   194       'prop' options prop |
   195       'term' options term |
   196       'const' options term |
   197       'abbrev' options term |
   198       'typeof' options term |
   199       'typ' options type |
   200       'thm\_style' options name thmref |
   201       'term\_style' options name term |
   202       'text' options name |
   203       'goals' options |
   204       'subgoals' options |
   205       'prf' options thmrefs |
   206       'full\_prf' options thmrefs |
   207       'ML' options name |
   208       'ML\_type' options name |
   209       'ML\_struct' options name
   210     ;
   211     options: '[' (option * ',') ']'
   212     ;
   213     option: name | name '=' name
   214     ;
   215   \end{rail}
   216 
   217   Note that the syntax of antiquotations may \emph{not} include source
   218   comments \verb|(*|~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\verb|*)| or verbatim
   219   text \verb|{|\verb|*|~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\verb|*|\verb|}|.
   220 
   221   \begin{descr}
   222   
   223   \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}theory\ A{\isacharbraceright}{\isachardoublequote}}] prints the name \isa{{\isachardoublequote}A{\isachardoublequote}}, which is
   224   guaranteed to refer to a valid ancestor theory in the current
   225   context.
   226 
   227   \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] prints theorems
   228   \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}.  Note that attribute specifications
   229   may be included as well (see also \secref{sec:syn-att}); the
   230   \indexref{}{attribute}{no\_vars}\hyperlink{attribute.no-vars}{\mbox{\isa{no{\isacharunderscore}vars}}} rule (see \secref{sec:misc-meth-att}) would
   231   be particularly useful to suppress printing of schematic variables.
   232 
   233   \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prop\ {\isasymphi}{\isacharbraceright}{\isachardoublequote}}] prints a well-typed proposition \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}.
   234 
   235   \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}lemma\ {\isasymphi}\ by\ m{\isacharbraceright}{\isachardoublequote}}] asserts a well-typed proposition \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}} to be provable by method \isa{m} and prints \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}.
   236 
   237   \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ t{\isacharbraceright}{\isachardoublequote}}] prints a well-typed term \isa{{\isachardoublequote}t{\isachardoublequote}}.
   238 
   239   \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}const\ c{\isacharbraceright}{\isachardoublequote}}] prints a logical or syntactic constant
   240   \isa{{\isachardoublequote}c{\isachardoublequote}}.
   241   
   242   \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}abbrev\ c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] prints a constant
   243   abbreviation \isa{{\isachardoublequote}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ rhs{\isachardoublequote}} as defined in
   244   the current context.
   245 
   246   \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typeof\ t{\isacharbraceright}{\isachardoublequote}}] prints the type of a well-typed term
   247   \isa{{\isachardoublequote}t{\isachardoublequote}}.
   248 
   249   \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typ\ {\isasymtau}{\isacharbraceright}{\isachardoublequote}}] prints a well-formed type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}.
   250   
   251   \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm{\isacharunderscore}style\ s\ a{\isacharbraceright}{\isachardoublequote}}] prints theorem \isa{a},
   252   previously applying a style \isa{s} to it (see below).
   253   
   254   \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).
   255 
   256   \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
   257   to the Isabelle {\LaTeX} output style, without demanding
   258   well-formedness (e.g.\ small pieces of terms that should not be
   259   parsed or type-checked yet).
   260 
   261   \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}goals{\isacharbraceright}{\isachardoublequote}}] prints the current \emph{dynamic} goal
   262   state.  This is mainly for support of tactic-emulation scripts
   263   within Isar --- presentation of goal states does not conform to
   264   actual human-readable proof documents.
   265 
   266   Please do not include goal states into document output unless you
   267   really know what you are doing!
   268   
   269   \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}subgoals{\isacharbraceright}{\isachardoublequote}}] is similar to \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}goals{\isacharbraceright}{\isachardoublequote}}, but
   270   does not print the main goal.
   271   
   272   \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] prints the (compact)
   273   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
   274   for the current object logic (see the ``Proof terms'' section of the
   275   Isabelle reference manual for information on how to do this).
   276   
   277   \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,
   278   i.e.\ also displays information omitted in the compact proof term,
   279   which is denoted by ``\isa{{\isacharunderscore}}'' placeholders there.
   280   
   281   \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
   282   structure, respectively.  The source is displayed verbatim.
   283 
   284   \end{descr}
   285 
   286   \medskip The following standard styles for use with \isa{thm{\isacharunderscore}style} and \isa{term{\isacharunderscore}style} are available:
   287 
   288   \begin{descr}
   289   
   290   \item [\isa{lhs}] extracts the first argument of any application
   291   form with at least two arguments -- typically meta-level or
   292   object-level equality, or any other binary relation.
   293   
   294   \item [\isa{rhs}] is like \isa{lhs}, but extracts the second
   295   argument.
   296   
   297   \item [\isa{{\isachardoublequote}concl{\isachardoublequote}}] extracts the conclusion \isa{C} from a rule
   298   in Horn-clause normal form \isa{{\isachardoublequote}A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C{\isachardoublequote}}.
   299   
   300   \item [\isa{{\isachardoublequote}prem{\isadigit{1}}{\isachardoublequote}}, \dots, \isa{{\isachardoublequote}prem{\isadigit{9}}{\isachardoublequote}}] extract premise
   301   number \isa{{\isachardoublequote}{\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isadigit{9}}{\isachardoublequote}}, respectively, from from a rule in
   302   Horn-clause normal form \isa{{\isachardoublequote}A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C{\isachardoublequote}}
   303 
   304   \end{descr}
   305 
   306   \medskip
   307   The following options are available to tune the output.  Note that most of
   308   these coincide with ML flags of the same names (see also \cite{isabelle-ref}).
   309 
   310   \begin{descr}
   311 
   312   \item[\isa{{\isachardoublequote}show{\isacharunderscore}types\ {\isacharequal}\ bool{\isachardoublequote}} and \isa{{\isachardoublequote}show{\isacharunderscore}sorts\ {\isacharequal}\ bool{\isachardoublequote}}]
   313   control printing of explicit type and sort constraints.
   314 
   315   \item[\isa{{\isachardoublequote}show{\isacharunderscore}structs\ {\isacharequal}\ bool{\isachardoublequote}}] controls printing of implicit
   316   structures.
   317 
   318   \item[\isa{{\isachardoublequote}long{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}}] forces names of types and
   319   constants etc.\ to be printed in their fully qualified internal
   320   form.
   321 
   322   \item[\isa{{\isachardoublequote}short{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}}] forces names of types and
   323   constants etc.\ to be printed unqualified.  Note that internalizing
   324   the output again in the current context may well yield a different
   325   result.
   326 
   327   \item[\isa{{\isachardoublequote}unique{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}}] determines whether the printed
   328   version of qualified names should be made sufficiently long to avoid
   329   overlap with names declared further back.  Set to \isa{false} for
   330   more concise output.
   331 
   332   \item[\isa{{\isachardoublequote}eta{\isacharunderscore}contract\ {\isacharequal}\ bool{\isachardoublequote}}] prints terms in \isa{{\isasymeta}}-contracted form.
   333 
   334   \item[\isa{{\isachardoublequote}display\ {\isacharequal}\ bool{\isachardoublequote}}] indicates if the text is to be
   335   output as multi-line ``display material'', rather than a small piece
   336   of text without line breaks (which is the default).
   337 
   338   \item[\isa{{\isachardoublequote}break\ {\isacharequal}\ bool{\isachardoublequote}}] controls line breaks in non-display
   339   material.
   340 
   341   \item[\isa{{\isachardoublequote}quotes\ {\isacharequal}\ bool{\isachardoublequote}}] indicates if the output should be
   342   enclosed in double quotes.
   343 
   344   \item[\isa{{\isachardoublequote}mode\ {\isacharequal}\ name{\isachardoublequote}}] adds \isa{name} to the print mode to
   345   be used for presentation (see also \cite{isabelle-ref}).  Note that
   346   the standard setup for {\LaTeX} output is already present by
   347   default, including the modes \isa{latex} and \isa{xsymbols}.
   348 
   349   \item[\isa{{\isachardoublequote}margin\ {\isacharequal}\ nat{\isachardoublequote}} and \isa{{\isachardoublequote}indent\ {\isacharequal}\ nat{\isachardoublequote}}] change the
   350   margin or indentation for pretty printing of display material.
   351 
   352   \item[\isa{{\isachardoublequote}source\ {\isacharequal}\ bool{\isachardoublequote}}] prints the source text of the
   353   antiquotation arguments, rather than the actual value.  Note that
   354   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).
   355 
   356   \item[\isa{{\isachardoublequote}goals{\isacharunderscore}limit\ {\isacharequal}\ nat{\isachardoublequote}}] determines the maximum number of
   357   goals to be printed.
   358 
   359   \item[\isa{{\isachardoublequote}locale\ {\isacharequal}\ name{\isachardoublequote}}] specifies an alternative locale
   360   context used for evaluating and printing the subsequent argument.
   361 
   362   \end{descr}
   363 
   364   For boolean flags, ``\isa{{\isachardoublequote}name\ {\isacharequal}\ true{\isachardoublequote}}'' may be abbreviated as
   365   ``\isa{name}''.  All of the above flags are disabled by default,
   366   unless changed from ML.
   367 
   368   \medskip Note that antiquotations do not only spare the author from
   369   tedious typing of logical entities, but also achieve some degree of
   370   consistency-checking of informal explanations with formal
   371   developments: well-formedness of terms and types with respect to the
   372   current theory or proof context is ensured here.%
   373 \end{isamarkuptext}%
   374 \isamarkuptrue%
   375 %
   376 \isamarkupsection{Tagged commands \label{sec:tags}%
   377 }
   378 \isamarkuptrue%
   379 %
   380 \begin{isamarkuptext}%
   381 Each Isabelle/Isar command may be decorated by presentation tags:
   382 
   383   \indexouternonterm{tags}
   384   \begin{rail}
   385     tags: ( tag * )
   386     ;
   387     tag: '\%' (ident | string)
   388   \end{rail}
   389 
   390   The tags \isa{{\isachardoublequote}theory{\isachardoublequote}}, \isa{{\isachardoublequote}proof{\isachardoublequote}}, \isa{{\isachardoublequote}ML{\isachardoublequote}} are already
   391   pre-declared for certain classes of commands:
   392 
   393  \medskip
   394 
   395   \begin{tabular}{ll}
   396     \isa{{\isachardoublequote}theory{\isachardoublequote}} & theory begin/end \\
   397     \isa{{\isachardoublequote}proof{\isachardoublequote}} & all proof commands \\
   398     \isa{{\isachardoublequote}ML{\isachardoublequote}} & all commands involving ML code \\
   399   \end{tabular}
   400 
   401   \medskip The Isabelle document preparation system (see also
   402   \cite{isabelle-sys}) allows tagged command regions to be presented
   403   specifically, e.g.\ to fold proof texts, or drop parts of the text
   404   completely.
   405 
   406   For example ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharpercent}invisible\ auto{\isachardoublequote}}'' would
   407   cause that piece of proof to be treated as \isa{invisible} instead
   408   of \isa{{\isachardoublequote}proof{\isachardoublequote}} (the default), which may be either show or hidden
   409   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
   410   invariably.
   411 
   412   Explicit tag specifications within a proof apply to all subsequent
   413   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
   414   whole sub-proof to be typeset as \isa{visible} (unless some of its
   415   parts are tagged differently).%
   416 \end{isamarkuptext}%
   417 \isamarkuptrue%
   418 %
   419 \isamarkupsection{Draft presentation%
   420 }
   421 \isamarkuptrue%
   422 %
   423 \begin{isamarkuptext}%
   424 \begin{matharray}{rcl}
   425     \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} \\
   426     \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} \\
   427   \end{matharray}
   428 
   429   \begin{rail}
   430     ('display\_drafts' | 'print\_drafts') (name +)
   431     ;
   432   \end{rail}
   433 
   434   \begin{descr}
   435 
   436   \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
   437   of raw source files.  Only those symbols that do not require
   438   additional {\LaTeX} packages are displayed properly, everything else
   439   is left verbatim.
   440 
   441   \end{descr}%
   442 \end{isamarkuptext}%
   443 \isamarkuptrue%
   444 %
   445 \isadelimtheory
   446 %
   447 \endisadelimtheory
   448 %
   449 \isatagtheory
   450 \isacommand{end}\isamarkupfalse%
   451 %
   452 \endisatagtheory
   453 {\isafoldtheory}%
   454 %
   455 \isadelimtheory
   456 %
   457 \endisadelimtheory
   458 \isanewline
   459 \end{isabellebody}%
   460 %%% Local Variables:
   461 %%% mode: latex
   462 %%% TeX-master: "root"
   463 %%% End: