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