doc-src/IsarRef/Thy/document/Document_Preparation.tex
author wenzelm
Fri Oct 29 11:49:56 2010 +0200 (2010-10-29)
changeset 40255 9ffbc25e1606
parent 39689 78b185bf7660
child 40406 313a24b66a8d
permissions -rw-r--r--
eliminated obsolete \_ escapes in rail environments;
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
%
wenzelm@27042
     7
\endisadelimtheory
wenzelm@27042
     8
%
wenzelm@27042
     9
\isatagtheory
wenzelm@27042
    10
\isacommand{theory}\isamarkupfalse%
wenzelm@27042
    11
\ Document{\isacharunderscore}Preparation\isanewline
wenzelm@27042
    12
\isakeyword{imports}\ Main\isanewline
wenzelm@27042
    13
\isakeyword{begin}%
wenzelm@27042
    14
\endisatagtheory
wenzelm@27042
    15
{\isafoldtheory}%
wenzelm@27042
    16
%
wenzelm@27042
    17
\isadelimtheory
wenzelm@27042
    18
%
wenzelm@27042
    19
\endisadelimtheory
wenzelm@27042
    20
%
wenzelm@27042
    21
\isamarkupchapter{Document preparation \label{ch:document-prep}%
wenzelm@27042
    22
}
wenzelm@27042
    23
\isamarkuptrue%
wenzelm@27042
    24
%
wenzelm@27042
    25
\begin{isamarkuptext}%
wenzelm@28788
    26
Isabelle/Isar provides a simple document preparation system
wenzelm@28788
    27
  based on regular {PDF-\LaTeX} technology, with full support for
wenzelm@28788
    28
  hyper-links and bookmarks.  Thus the results are well suited for WWW
wenzelm@28788
    29
  browsing and as printed copies.
wenzelm@27042
    30
wenzelm@28788
    31
  \medskip Isabelle generates {\LaTeX} output while running a
wenzelm@27042
    32
  \emph{logic session} (see also \cite{isabelle-sys}).  Getting
wenzelm@27042
    33
  started with a working configuration for common situations is quite
wenzelm@27042
    34
  easy by using the Isabelle \verb|mkdir| and \verb|make|
wenzelm@27042
    35
  tools.  First invoke
wenzelm@27042
    36
\begin{ttbox}
wenzelm@28505
    37
  isabelle mkdir Foo
wenzelm@27042
    38
\end{ttbox}
wenzelm@28788
    39
  to initialize a separate directory for session \verb|Foo| (it
wenzelm@28788
    40
  is safe to experiment, since \verb|isabelle mkdir| never
wenzelm@28788
    41
  overwrites existing files).  Ensure that \verb|Foo/ROOT.ML|
wenzelm@27042
    42
  holds ML commands to load all theories required for this session;
wenzelm@27042
    43
  furthermore \verb|Foo/document/root.tex| should include any
wenzelm@27042
    44
  special {\LaTeX} macro packages required for your document (the
wenzelm@27042
    45
  default is usually sufficient as a start).
wenzelm@27042
    46
wenzelm@27042
    47
  The session is controlled by a separate \verb|IsaMakefile|
wenzelm@27042
    48
  (with crude source dependencies by default).  This file is located
wenzelm@27042
    49
  one level up from the \verb|Foo| directory location.  Now
wenzelm@27042
    50
  invoke
wenzelm@27042
    51
\begin{ttbox}
wenzelm@28505
    52
  isabelle make Foo
wenzelm@27042
    53
\end{ttbox}
wenzelm@27042
    54
  to run the \verb|Foo| session, with browser information and
wenzelm@27042
    55
  document preparation enabled.  Unless any errors are reported by
wenzelm@27042
    56
  Isabelle or {\LaTeX}, the output will appear inside the directory
wenzelm@28788
    57
  defined by the \verb|ISABELLE_BROWSER_INFO| setting (as
wenzelm@28788
    58
  reported by the batch job in verbose mode).
wenzelm@27042
    59
wenzelm@27042
    60
  \medskip You may also consider to tune the \verb|usedir|
wenzelm@28788
    61
  options in \verb|IsaMakefile|, for example to switch the output
wenzelm@28788
    62
  format between \verb|pdf| and \verb|dvi|, or activate the
wenzelm@27042
    63
  \verb|-D| option to retain a second copy of the generated
wenzelm@28788
    64
  {\LaTeX} sources (for manual inspection or separate runs of
wenzelm@28788
    65
  \hyperlink{executable.latex}{\mbox{\isa{\isatt{latex}}}}).
wenzelm@27042
    66
wenzelm@27042
    67
  \medskip See \emph{The Isabelle System Manual} \cite{isabelle-sys}
wenzelm@27042
    68
  for further details on Isabelle logic sessions and theory
wenzelm@27042
    69
  presentation.  The Isabelle/HOL tutorial \cite{isabelle-hol-book}
wenzelm@28788
    70
  also covers theory presentation to some extent.%
wenzelm@27042
    71
\end{isamarkuptext}%
wenzelm@27042
    72
\isamarkuptrue%
wenzelm@27042
    73
%
wenzelm@27042
    74
\isamarkupsection{Markup commands \label{sec:markup}%
wenzelm@27042
    75
}
wenzelm@27042
    76
\isamarkuptrue%
wenzelm@27042
    77
%
wenzelm@27042
    78
\begin{isamarkuptext}%
wenzelm@27042
    79
\begin{matharray}{rcl}
wenzelm@28788
    80
    \indexdef{}{command}{header}\hypertarget{command.header}{\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}}} & : & \isa{{\isachardoublequote}toplevel\ {\isasymrightarrow}\ toplevel{\isachardoublequote}} \\[0.5ex]
wenzelm@28788
    81
    \indexdef{}{command}{chapter}\hypertarget{command.chapter}{\hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
wenzelm@28788
    82
    \indexdef{}{command}{section}\hypertarget{command.section}{\hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
wenzelm@28788
    83
    \indexdef{}{command}{subsection}\hypertarget{command.subsection}{\hyperlink{command.subsection}{\mbox{\isa{\isacommand{subsection}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
wenzelm@28788
    84
    \indexdef{}{command}{subsubsection}\hypertarget{command.subsubsection}{\hyperlink{command.subsubsection}{\mbox{\isa{\isacommand{subsubsection}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
wenzelm@28788
    85
    \indexdef{}{command}{text}\hypertarget{command.text}{\hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
wenzelm@28788
    86
    \indexdef{}{command}{text\_raw}\hypertarget{command.text-raw}{\hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\[0.5ex]
wenzelm@28788
    87
    \indexdef{}{command}{sect}\hypertarget{command.sect}{\hyperlink{command.sect}{\mbox{\isa{\isacommand{sect}}}}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}\ proof{\isachardoublequote}} \\
wenzelm@28788
    88
    \indexdef{}{command}{subsect}\hypertarget{command.subsect}{\hyperlink{command.subsect}{\mbox{\isa{\isacommand{subsect}}}}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}\ proof{\isachardoublequote}} \\
wenzelm@28788
    89
    \indexdef{}{command}{subsubsect}\hypertarget{command.subsubsect}{\hyperlink{command.subsubsect}{\mbox{\isa{\isacommand{subsubsect}}}}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}\ proof{\isachardoublequote}} \\
wenzelm@28788
    90
    \indexdef{}{command}{txt}\hypertarget{command.txt}{\hyperlink{command.txt}{\mbox{\isa{\isacommand{txt}}}}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}\ proof{\isachardoublequote}} \\
wenzelm@28788
    91
    \indexdef{}{command}{txt\_raw}\hypertarget{command.txt-raw}{\hyperlink{command.txt-raw}{\mbox{\isa{\isacommand{txt{\isacharunderscore}raw}}}}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}\ proof{\isachardoublequote}} \\
wenzelm@27042
    92
  \end{matharray}
wenzelm@27042
    93
wenzelm@28788
    94
  Markup commands provide a structured way to insert text into the
wenzelm@28788
    95
  document generated from a theory.  Each markup command takes a
wenzelm@28788
    96
  single \hyperlink{syntax.text}{\mbox{\isa{text}}} argument, which is passed as argument to a
wenzelm@28788
    97
  corresponding {\LaTeX} macro.  The default macros provided by
wenzelm@28788
    98
  \hyperlink{file.~~/lib/texinputs/isabelle.sty}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}lib{\isacharslash}texinputs{\isacharslash}isabelle{\isachardot}sty}}}} can be redefined according
wenzelm@28788
    99
  to the needs of the underlying document and {\LaTeX} styles.
wenzelm@28788
   100
wenzelm@28788
   101
  Note that formal comments (\secref{sec:comments}) are similar to
wenzelm@28788
   102
  markup commands, but have a different status within Isabelle/Isar
wenzelm@28788
   103
  syntax.
wenzelm@27042
   104
wenzelm@27042
   105
  \begin{rail}
wenzelm@27042
   106
    ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
wenzelm@27042
   107
    ;
wenzelm@40255
   108
    ('header' | 'text_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt_raw') text
wenzelm@27042
   109
    ;
wenzelm@27042
   110
  \end{rail}
wenzelm@27042
   111
wenzelm@28788
   112
  \begin{description}
wenzelm@27042
   113
wenzelm@28788
   114
  \item \hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}} provides plain text markup just preceding
wenzelm@28788
   115
  the formal beginning of a theory.  The corresponding {\LaTeX} macro
wenzelm@28788
   116
  is \verb|\isamarkupheader|, which acts like \hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}} by default.
wenzelm@27052
   117
  
wenzelm@28788
   118
  \item \hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}, \hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}}, \hyperlink{command.subsection}{\mbox{\isa{\isacommand{subsection}}}},
wenzelm@28788
   119
  and \hyperlink{command.subsubsection}{\mbox{\isa{\isacommand{subsubsection}}}} mark chapter and section headings
wenzelm@28788
   120
  within the main theory body or local theory targets.  The
wenzelm@28788
   121
  corresponding {\LaTeX} macros are \verb|\isamarkupchapter|,
wenzelm@28788
   122
  \verb|\isamarkupsection|, \verb|\isamarkupsubsection| etc.
wenzelm@27042
   123
wenzelm@28788
   124
  \item \hyperlink{command.sect}{\mbox{\isa{\isacommand{sect}}}}, \hyperlink{command.subsect}{\mbox{\isa{\isacommand{subsect}}}}, and \hyperlink{command.subsubsect}{\mbox{\isa{\isacommand{subsubsect}}}}
wenzelm@28788
   125
  mark section headings within proofs.  The corresponding {\LaTeX}
wenzelm@28788
   126
  macros are \verb|\isamarkupsect|, \verb|\isamarkupsubsect| etc.
wenzelm@27042
   127
wenzelm@28788
   128
  \item \hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}} and \hyperlink{command.txt}{\mbox{\isa{\isacommand{txt}}}} specify paragraphs of plain
wenzelm@28788
   129
  text.  This corresponds to a {\LaTeX} environment \verb|\begin{isamarkuptext}| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|\end{isamarkuptext}| etc.
wenzelm@27042
   130
wenzelm@28788
   131
  \item \hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}} and \hyperlink{command.txt-raw}{\mbox{\isa{\isacommand{txt{\isacharunderscore}raw}}}} insert {\LaTeX}
wenzelm@28788
   132
  source into the output, without additional markup.  Thus the full
wenzelm@28788
   133
  range of document manipulations becomes available, at the risk of
wenzelm@28788
   134
  messing up document output.
wenzelm@27042
   135
wenzelm@28788
   136
  \end{description}
wenzelm@27042
   137
wenzelm@28788
   138
  Except for \hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}} and \hyperlink{command.txt-raw}{\mbox{\isa{\isacommand{txt{\isacharunderscore}raw}}}}, the text
wenzelm@28788
   139
  passed to any of the above markup commands may refer to formal
wenzelm@28788
   140
  entities via \emph{document antiquotations}, see also
wenzelm@28788
   141
  \secref{sec:antiq}.  These are interpreted in the present theory or
wenzelm@28788
   142
  proof context, or the named \isa{{\isachardoublequote}target{\isachardoublequote}}.
wenzelm@27042
   143
wenzelm@27042
   144
  \medskip The proof markup commands closely resemble those for theory
wenzelm@27042
   145
  specifications, but have a different formal status and produce
wenzelm@28788
   146
  different {\LaTeX} macros.  The default definitions coincide for
wenzelm@28788
   147
  analogous commands such as \hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}} and \hyperlink{command.sect}{\mbox{\isa{\isacommand{sect}}}}.%
wenzelm@27042
   148
\end{isamarkuptext}%
wenzelm@27042
   149
\isamarkuptrue%
wenzelm@27042
   150
%
wenzelm@28788
   151
\isamarkupsection{Document Antiquotations \label{sec:antiq}%
wenzelm@27042
   152
}
wenzelm@27042
   153
\isamarkuptrue%
wenzelm@27042
   154
%
wenzelm@27042
   155
\begin{isamarkuptext}%
wenzelm@27042
   156
\begin{matharray}{rcl}
wenzelm@28788
   157
    \indexdef{}{antiquotation}{theory}\hypertarget{antiquotation.theory}{\hyperlink{antiquotation.theory}{\mbox{\isa{theory}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   158
    \indexdef{}{antiquotation}{thm}\hypertarget{antiquotation.thm}{\hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   159
    \indexdef{}{antiquotation}{lemma}\hypertarget{antiquotation.lemma}{\hyperlink{antiquotation.lemma}{\mbox{\isa{lemma}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   160
    \indexdef{}{antiquotation}{prop}\hypertarget{antiquotation.prop}{\hyperlink{antiquotation.prop}{\mbox{\isa{prop}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   161
    \indexdef{}{antiquotation}{term}\hypertarget{antiquotation.term}{\hyperlink{antiquotation.term}{\mbox{\isa{term}}}} & : & \isa{antiquotation} \\
haftmann@32898
   162
    \indexdef{}{antiquotation}{term\_type}\hypertarget{antiquotation.term-type}{\hyperlink{antiquotation.term-type}{\mbox{\isa{term{\isacharunderscore}type}}}} & : & \isa{antiquotation} \\
haftmann@32898
   163
    \indexdef{}{antiquotation}{typeof}\hypertarget{antiquotation.typeof}{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   164
    \indexdef{}{antiquotation}{const}\hypertarget{antiquotation.const}{\hyperlink{antiquotation.const}{\mbox{\isa{const}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   165
    \indexdef{}{antiquotation}{abbrev}\hypertarget{antiquotation.abbrev}{\hyperlink{antiquotation.abbrev}{\mbox{\isa{abbrev}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   166
    \indexdef{}{antiquotation}{typ}\hypertarget{antiquotation.typ}{\hyperlink{antiquotation.typ}{\mbox{\isa{typ}}}} & : & \isa{antiquotation} \\
wenzelm@39437
   167
    \indexdef{}{antiquotation}{type}\hypertarget{antiquotation.type}{\hyperlink{antiquotation.type}{\mbox{\isa{type}}}} & : & \isa{antiquotation} \\
wenzelm@39437
   168
    \indexdef{}{antiquotation}{class}\hypertarget{antiquotation.class}{\hyperlink{antiquotation.class}{\mbox{\isa{class}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   169
    \indexdef{}{antiquotation}{text}\hypertarget{antiquotation.text}{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   170
    \indexdef{}{antiquotation}{goals}\hypertarget{antiquotation.goals}{\hyperlink{antiquotation.goals}{\mbox{\isa{goals}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   171
    \indexdef{}{antiquotation}{subgoals}\hypertarget{antiquotation.subgoals}{\hyperlink{antiquotation.subgoals}{\mbox{\isa{subgoals}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   172
    \indexdef{}{antiquotation}{prf}\hypertarget{antiquotation.prf}{\hyperlink{antiquotation.prf}{\mbox{\isa{prf}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   173
    \indexdef{}{antiquotation}{full\_prf}\hypertarget{antiquotation.full-prf}{\hyperlink{antiquotation.full-prf}{\mbox{\isa{full{\isacharunderscore}prf}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   174
    \indexdef{}{antiquotation}{ML}\hypertarget{antiquotation.ML}{\hyperlink{antiquotation.ML}{\mbox{\isa{ML}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   175
    \indexdef{}{antiquotation}{ML\_type}\hypertarget{antiquotation.ML-type}{\hyperlink{antiquotation.ML-type}{\mbox{\isa{ML{\isacharunderscore}type}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   176
    \indexdef{}{antiquotation}{ML\_struct}\hypertarget{antiquotation.ML-struct}{\hyperlink{antiquotation.ML-struct}{\mbox{\isa{ML{\isacharunderscore}struct}}}} & : & \isa{antiquotation} \\
wenzelm@27042
   177
  \end{matharray}
wenzelm@27042
   178
wenzelm@28788
   179
  The overall content of an Isabelle/Isar theory may alternate between
wenzelm@28788
   180
  formal and informal text.  The main body consists of formal
wenzelm@28788
   181
  specification and proof commands, interspersed with markup commands
wenzelm@28788
   182
  (\secref{sec:markup}) or document comments (\secref{sec:comments}).
wenzelm@28788
   183
  The argument of markup commands quotes informal text to be printed
wenzelm@28788
   184
  in the resulting document, but may again refer to formal entities
wenzelm@28788
   185
  via \emph{document antiquotations}.
wenzelm@27042
   186
wenzelm@28788
   187
  For example, embedding of ``\isa{{\isacharat}{\isacharbraceleft}term\ {\isacharbrackleft}show{\isacharunderscore}types{\isacharbrackright}\ {\isachardoublequote}f\ x\ {\isacharequal}\ a\ {\isacharplus}\ x{\isachardoublequote}{\isacharbraceright}}''
wenzelm@28788
   188
  within a text block makes
wenzelm@28788
   189
  \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} appear in the final {\LaTeX} document.
wenzelm@28788
   190
wenzelm@28788
   191
  Antiquotations usually spare the author tedious typing of logical
wenzelm@28788
   192
  entities in full detail.  Even more importantly, some degree of
wenzelm@28788
   193
  consistency-checking between the main body of formal text and its
wenzelm@28788
   194
  informal explanation is achieved, since terms and types appearing in
wenzelm@28788
   195
  antiquotations are checked within the current theory or proof
wenzelm@28788
   196
  context.
wenzelm@27042
   197
wenzelm@27042
   198
  \begin{rail}
wenzelm@27042
   199
    atsign lbrace antiquotation rbrace
wenzelm@27042
   200
    ;
wenzelm@27042
   201
wenzelm@27042
   202
    antiquotation:
wenzelm@27042
   203
      'theory' options name |
haftmann@32893
   204
      'thm' options styles thmrefs |
haftmann@27453
   205
      'lemma' options prop 'by' method |
haftmann@32893
   206
      'prop' options styles prop |
haftmann@32893
   207
      'term' options styles term |
haftmann@32898
   208
      'term_type' options styles term |
haftmann@32898
   209
      'typeof' options styles term |
wenzelm@27042
   210
      'const' options term |
wenzelm@27042
   211
      'abbrev' options term |
wenzelm@27042
   212
      'typ' options type |
wenzelm@39437
   213
      'type' options name |
wenzelm@39437
   214
      'class' options name |
wenzelm@27042
   215
      'text' options name |
wenzelm@27042
   216
      'goals' options |
wenzelm@27042
   217
      'subgoals' options |
wenzelm@27042
   218
      'prf' options thmrefs |
wenzelm@40255
   219
      'full_prf' options thmrefs |
wenzelm@27042
   220
      'ML' options name |
wenzelm@40255
   221
      'ML_type' options name |
wenzelm@40255
   222
      'ML_struct' options name
wenzelm@27042
   223
    ;
wenzelm@27042
   224
    options: '[' (option * ',') ']'
wenzelm@27042
   225
    ;
wenzelm@27042
   226
    option: name | name '=' name
wenzelm@27042
   227
    ;
haftmann@32893
   228
    styles: '(' (style + ',') ')'
haftmann@32893
   229
    ;
haftmann@32893
   230
    style: (name +)
haftmann@32893
   231
    ;
wenzelm@27042
   232
  \end{rail}
wenzelm@27042
   233
wenzelm@27042
   234
  Note that the syntax of antiquotations may \emph{not} include source
wenzelm@28788
   235
  comments \verb|(*|~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\verb|*)| nor verbatim
wenzelm@27042
   236
  text \verb|{|\verb|*|~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\verb|*|\verb|}|.
wenzelm@27042
   237
wenzelm@28788
   238
  \begin{description}
wenzelm@27042
   239
  
wenzelm@28788
   240
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}theory\ A{\isacharbraceright}{\isachardoublequote}} prints the name \isa{{\isachardoublequote}A{\isachardoublequote}}, which is
wenzelm@27042
   241
  guaranteed to refer to a valid ancestor theory in the current
wenzelm@27042
   242
  context.
wenzelm@27042
   243
wenzelm@28788
   244
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}} prints theorems \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}.
wenzelm@28788
   245
  Full fact expressions are allowed here, including attributes
wenzelm@28788
   246
  (\secref{sec:syn-att}).
wenzelm@28788
   247
wenzelm@28788
   248
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prop\ {\isasymphi}{\isacharbraceright}{\isachardoublequote}} prints a well-typed proposition \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}.
wenzelm@27042
   249
wenzelm@28788
   250
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}lemma\ {\isasymphi}\ by\ m{\isacharbraceright}{\isachardoublequote}} proves a well-typed proposition
wenzelm@28788
   251
  \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}} by method \isa{m} and prints the original \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}.
haftmann@27453
   252
wenzelm@28788
   253
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ t{\isacharbraceright}{\isachardoublequote}} prints a well-typed term \isa{{\isachardoublequote}t{\isachardoublequote}}.
wenzelm@27042
   254
haftmann@32898
   255
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term{\isacharunderscore}type\ t{\isacharbraceright}{\isachardoublequote}} prints a well-typed term \isa{{\isachardoublequote}t{\isachardoublequote}}
haftmann@32898
   256
  annotated with its type.
haftmann@32898
   257
haftmann@32898
   258
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typeof\ t{\isacharbraceright}{\isachardoublequote}} prints the type of a well-typed term
haftmann@32898
   259
  \isa{{\isachardoublequote}t{\isachardoublequote}}.
haftmann@32898
   260
wenzelm@28788
   261
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}const\ c{\isacharbraceright}{\isachardoublequote}} prints a logical or syntactic constant
wenzelm@27042
   262
  \isa{{\isachardoublequote}c{\isachardoublequote}}.
wenzelm@27042
   263
  
wenzelm@28788
   264
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}abbrev\ c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isacharbraceright}{\isachardoublequote}} prints a constant abbreviation
wenzelm@28788
   265
  \isa{{\isachardoublequote}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ rhs{\isachardoublequote}} as defined in the current context.
wenzelm@39437
   266
wenzelm@28788
   267
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typ\ {\isasymtau}{\isacharbraceright}{\isachardoublequote}} prints a well-formed type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}.
wenzelm@39437
   268
wenzelm@39689
   269
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}type\ {\isasymkappa}{\isacharbraceright}{\isachardoublequote}} prints a (logical or syntactic) type
wenzelm@39689
   270
    constructor \isa{{\isachardoublequote}{\isasymkappa}{\isachardoublequote}}.
wenzelm@39437
   271
wenzelm@39437
   272
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}class\ c{\isacharbraceright}{\isachardoublequote}} prints a class \isa{c}.
wenzelm@39437
   273
wenzelm@28788
   274
  \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@28788
   275
  to the Isabelle document style, without demanding well-formedness,
wenzelm@28788
   276
  e.g.\ small pieces of terms that should not be parsed or
wenzelm@28788
   277
  type-checked yet.
wenzelm@27042
   278
wenzelm@28788
   279
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}goals{\isacharbraceright}{\isachardoublequote}} prints the current \emph{dynamic} goal
wenzelm@27042
   280
  state.  This is mainly for support of tactic-emulation scripts
wenzelm@28788
   281
  within Isar.  Presentation of goal states does not conform to the
wenzelm@28788
   282
  idea of human-readable proof documents!
wenzelm@27042
   283
wenzelm@28788
   284
  When explaining proofs in detail it is usually better to spell out
wenzelm@28788
   285
  the reasoning via proper Isar proof commands, instead of peeking at
wenzelm@28788
   286
  the internal machine configuration.
wenzelm@27042
   287
  
wenzelm@28788
   288
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}subgoals{\isacharbraceright}{\isachardoublequote}} is similar to \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}goals{\isacharbraceright}{\isachardoublequote}}, but
wenzelm@27042
   289
  does not print the main goal.
wenzelm@27042
   290
  
wenzelm@28788
   291
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}} prints the (compact) proof terms
wenzelm@28788
   292
  corresponding to the theorems \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}. Note that this
wenzelm@28788
   293
  requires proof terms to be switched on for the current logic
wenzelm@28788
   294
  session.
wenzelm@27042
   295
  
wenzelm@28788
   296
  \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 prints the full proof terms, i.e.\ also displays
wenzelm@28788
   297
  information omitted in the compact proof term, which is denoted by
wenzelm@28788
   298
  ``\isa{{\isacharunderscore}}'' placeholders there.
wenzelm@27042
   299
  
wenzelm@28788
   300
  \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@28788
   301
  structure, respectively.  The source is printed verbatim.
wenzelm@27042
   302
wenzelm@28788
   303
  \end{description}%
wenzelm@28788
   304
\end{isamarkuptext}%
wenzelm@28788
   305
\isamarkuptrue%
wenzelm@28788
   306
%
wenzelm@28788
   307
\isamarkupsubsubsection{Styled antiquotations%
wenzelm@28788
   308
}
wenzelm@28788
   309
\isamarkuptrue%
wenzelm@28788
   310
%
wenzelm@28788
   311
\begin{isamarkuptext}%
haftmann@32893
   312
The antiquotations \isa{thm}, \isa{prop} and \isa{term} admit an extra \emph{style} specification to modify the
haftmann@32893
   313
  printed result.  A style is specified by a name with a possibly
haftmann@32893
   314
  empty number of arguments;  multiple styles can be sequenced with
haftmann@32893
   315
  commas.  The following standard styles are available:
wenzelm@27042
   316
wenzelm@28788
   317
  \begin{description}
wenzelm@27042
   318
  
wenzelm@28788
   319
  \item \isa{lhs} extracts the first argument of any application
wenzelm@28788
   320
  form with at least two arguments --- typically meta-level or
wenzelm@27042
   321
  object-level equality, or any other binary relation.
wenzelm@27042
   322
  
wenzelm@28788
   323
  \item \isa{rhs} is like \isa{lhs}, but extracts the second
wenzelm@27042
   324
  argument.
wenzelm@27042
   325
  
wenzelm@28788
   326
  \item \isa{{\isachardoublequote}concl{\isachardoublequote}} extracts the conclusion \isa{C} from a rule
wenzelm@27042
   327
  in Horn-clause normal form \isa{{\isachardoublequote}A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C{\isachardoublequote}}.
wenzelm@27042
   328
  
haftmann@32893
   329
  \item \isa{{\isachardoublequote}prem{\isachardoublequote}} \isa{n} extract premise number
haftmann@32893
   330
  \isa{{\isachardoublequote}n{\isachardoublequote}} from from a rule in Horn-clause
wenzelm@28788
   331
  normal form \isa{{\isachardoublequote}A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C{\isachardoublequote}}
wenzelm@27042
   332
wenzelm@28788
   333
  \end{description}%
wenzelm@28788
   334
\end{isamarkuptext}%
wenzelm@28788
   335
\isamarkuptrue%
wenzelm@28788
   336
%
wenzelm@28788
   337
\isamarkupsubsubsection{General options%
wenzelm@28788
   338
}
wenzelm@28788
   339
\isamarkuptrue%
wenzelm@28788
   340
%
wenzelm@28788
   341
\begin{isamarkuptext}%
wenzelm@28788
   342
The following options are available to tune the printed output
wenzelm@28788
   343
  of antiquotations.  Note that many of these coincide with global ML
wenzelm@28788
   344
  flags of the same names.
wenzelm@27042
   345
wenzelm@28788
   346
  \begin{description}
wenzelm@27042
   347
wenzelm@30397
   348
  \item \indexdef{}{antiquotation option}{show\_types}\hypertarget{antiquotation option.show-types}{\hyperlink{antiquotation option.show-types}{\mbox{\isa{show{\isacharunderscore}types}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} and
wenzelm@30397
   349
  \indexdef{}{antiquotation option}{show\_sorts}\hypertarget{antiquotation option.show-sorts}{\hyperlink{antiquotation option.show-sorts}{\mbox{\isa{show{\isacharunderscore}sorts}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} control
wenzelm@30397
   350
  printing of explicit type and sort constraints.
wenzelm@27042
   351
wenzelm@30397
   352
  \item \indexdef{}{antiquotation option}{show\_structs}\hypertarget{antiquotation option.show-structs}{\hyperlink{antiquotation option.show-structs}{\mbox{\isa{show{\isacharunderscore}structs}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}}
wenzelm@30397
   353
  controls printing of implicit structures.
wenzelm@27042
   354
wenzelm@30397
   355
  \item \indexdef{}{antiquotation option}{long\_names}\hypertarget{antiquotation option.long-names}{\hyperlink{antiquotation option.long-names}{\mbox{\isa{long{\isacharunderscore}names}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} forces
wenzelm@30397
   356
  names of types and constants etc.\ to be printed in their fully
wenzelm@30397
   357
  qualified internal form.
wenzelm@27042
   358
wenzelm@30397
   359
  \item \indexdef{}{antiquotation option}{short\_names}\hypertarget{antiquotation option.short-names}{\hyperlink{antiquotation option.short-names}{\mbox{\isa{short{\isacharunderscore}names}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}}
wenzelm@30397
   360
  forces names of types and constants etc.\ to be printed unqualified.
wenzelm@30397
   361
  Note that internalizing the output again in the current context may
wenzelm@30397
   362
  well yield a different result.
wenzelm@27042
   363
wenzelm@30397
   364
  \item \indexdef{}{antiquotation option}{unique\_names}\hypertarget{antiquotation option.unique-names}{\hyperlink{antiquotation option.unique-names}{\mbox{\isa{unique{\isacharunderscore}names}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}}
wenzelm@30397
   365
  determines whether the printed version of qualified names should be
wenzelm@30397
   366
  made sufficiently long to avoid overlap with names declared further
wenzelm@30397
   367
  back.  Set to \isa{false} for more concise output.
wenzelm@27042
   368
wenzelm@30397
   369
  \item \indexdef{}{antiquotation option}{eta\_contract}\hypertarget{antiquotation option.eta-contract}{\hyperlink{antiquotation option.eta-contract}{\mbox{\isa{eta{\isacharunderscore}contract}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}}
wenzelm@30397
   370
  prints terms in \isa{{\isasymeta}}-contracted form.
wenzelm@27042
   371
wenzelm@30397
   372
  \item \indexdef{}{antiquotation option}{display}\hypertarget{antiquotation option.display}{\hyperlink{antiquotation option.display}{\mbox{\isa{display}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} indicates
wenzelm@30397
   373
  if the text is to be output as multi-line ``display material'',
wenzelm@30397
   374
  rather than a small piece of text without line breaks (which is the
wenzelm@30397
   375
  default).
wenzelm@27042
   376
wenzelm@28788
   377
  In this mode the embedded entities are printed in the same style as
wenzelm@28788
   378
  the main theory text.
wenzelm@28788
   379
wenzelm@30397
   380
  \item \indexdef{}{antiquotation option}{break}\hypertarget{antiquotation option.break}{\hyperlink{antiquotation option.break}{\mbox{\isa{break}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} controls
wenzelm@30397
   381
  line breaks in non-display material.
wenzelm@27042
   382
wenzelm@30397
   383
  \item \indexdef{}{antiquotation option}{quotes}\hypertarget{antiquotation option.quotes}{\hyperlink{antiquotation option.quotes}{\mbox{\isa{quotes}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} indicates
wenzelm@30397
   384
  if the output should be enclosed in double quotes.
wenzelm@27042
   385
wenzelm@30397
   386
  \item \indexdef{}{antiquotation option}{mode}\hypertarget{antiquotation option.mode}{\hyperlink{antiquotation option.mode}{\mbox{\isa{mode}}}}~\isa{{\isachardoublequote}{\isacharequal}\ name{\isachardoublequote}} adds \isa{name} to the print mode to be used for presentation.  Note that the
wenzelm@30397
   387
  standard setup for {\LaTeX} output is already present by default,
wenzelm@30397
   388
  including the modes \isa{latex} and \isa{xsymbols}.
wenzelm@27042
   389
wenzelm@30397
   390
  \item \indexdef{}{antiquotation option}{margin}\hypertarget{antiquotation option.margin}{\hyperlink{antiquotation option.margin}{\mbox{\isa{margin}}}}~\isa{{\isachardoublequote}{\isacharequal}\ nat{\isachardoublequote}} and
wenzelm@30397
   391
  \indexdef{}{antiquotation option}{indent}\hypertarget{antiquotation option.indent}{\hyperlink{antiquotation option.indent}{\mbox{\isa{indent}}}}~\isa{{\isachardoublequote}{\isacharequal}\ nat{\isachardoublequote}} change the margin
wenzelm@30397
   392
  or indentation for pretty printing of display material.
wenzelm@27042
   393
wenzelm@30397
   394
  \item \indexdef{}{antiquotation option}{goals\_limit}\hypertarget{antiquotation option.goals-limit}{\hyperlink{antiquotation option.goals-limit}{\mbox{\isa{goals{\isacharunderscore}limit}}}}~\isa{{\isachardoublequote}{\isacharequal}\ nat{\isachardoublequote}}
wenzelm@30397
   395
  determines the maximum number of goals to be printed (for goal-based
wenzelm@30397
   396
  antiquotation).
wenzelm@27042
   397
wenzelm@30397
   398
  \item \indexdef{}{antiquotation option}{source}\hypertarget{antiquotation option.source}{\hyperlink{antiquotation option.source}{\mbox{\isa{source}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} prints the
wenzelm@30397
   399
  original source text of the antiquotation arguments, rather than its
wenzelm@30397
   400
  internal representation.  Note that formal checking of
wenzelm@30397
   401
  \hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}, \hyperlink{antiquotation.term}{\mbox{\isa{term}}}, etc. is still
wenzelm@30397
   402
  enabled; use the \hyperlink{antiquotation.text}{\mbox{\isa{text}}} antiquotation for unchecked
wenzelm@30397
   403
  output.
wenzelm@28788
   404
wenzelm@28788
   405
  Regular \isa{{\isachardoublequote}term{\isachardoublequote}} and \isa{{\isachardoublequote}typ{\isachardoublequote}} antiquotations with \isa{{\isachardoublequote}source\ {\isacharequal}\ false{\isachardoublequote}} involve a full round-trip from the original source
wenzelm@28788
   406
  to an internalized logical entity back to a source form, according
wenzelm@28788
   407
  to the syntax of the current context.  Thus the printed output is
wenzelm@28788
   408
  not under direct control of the author, it may even fluctuate a bit
wenzelm@28788
   409
  as the underlying theory is changed later on.
wenzelm@28788
   410
wenzelm@30397
   411
  In contrast, \indexdef{}{antiquotation option}{source}\hypertarget{antiquotation option.source}{\hyperlink{antiquotation option.source}{\mbox{\isa{source}}}}~\isa{{\isachardoublequote}{\isacharequal}\ true{\isachardoublequote}}
wenzelm@30397
   412
  admits direct printing of the given source text, with the desirable
wenzelm@30397
   413
  well-formedness check in the background, but without modification of
wenzelm@30397
   414
  the printed text.
wenzelm@28788
   415
wenzelm@28788
   416
  \end{description}
wenzelm@27042
   417
wenzelm@27042
   418
  For boolean flags, ``\isa{{\isachardoublequote}name\ {\isacharequal}\ true{\isachardoublequote}}'' may be abbreviated as
wenzelm@27042
   419
  ``\isa{name}''.  All of the above flags are disabled by default,
wenzelm@28788
   420
  unless changed from ML, say in the \verb|ROOT.ML| of the
wenzelm@28788
   421
  logic session.%
wenzelm@27042
   422
\end{isamarkuptext}%
wenzelm@27042
   423
\isamarkuptrue%
wenzelm@27042
   424
%
wenzelm@28788
   425
\isamarkupsection{Markup via command tags \label{sec:tags}%
wenzelm@27042
   426
}
wenzelm@27042
   427
\isamarkuptrue%
wenzelm@27042
   428
%
wenzelm@27042
   429
\begin{isamarkuptext}%
wenzelm@28788
   430
Each Isabelle/Isar command may be decorated by additional
wenzelm@28788
   431
  presentation tags, to indicate some modification in the way it is
wenzelm@28788
   432
  printed in the document.
wenzelm@27042
   433
wenzelm@27042
   434
  \indexouternonterm{tags}
wenzelm@27042
   435
  \begin{rail}
wenzelm@27042
   436
    tags: ( tag * )
wenzelm@27042
   437
    ;
wenzelm@27042
   438
    tag: '\%' (ident | string)
wenzelm@27042
   439
  \end{rail}
wenzelm@27042
   440
wenzelm@28788
   441
  Some tags are pre-declared for certain classes of commands, serving
wenzelm@28788
   442
  as default markup if no tags are given in the text:
wenzelm@27042
   443
wenzelm@28788
   444
  \medskip
wenzelm@27042
   445
  \begin{tabular}{ll}
wenzelm@27042
   446
    \isa{{\isachardoublequote}theory{\isachardoublequote}} & theory begin/end \\
wenzelm@27042
   447
    \isa{{\isachardoublequote}proof{\isachardoublequote}} & all proof commands \\
wenzelm@27042
   448
    \isa{{\isachardoublequote}ML{\isachardoublequote}} & all commands involving ML code \\
wenzelm@27042
   449
  \end{tabular}
wenzelm@27042
   450
wenzelm@28788
   451
  \medskip The Isabelle document preparation system
wenzelm@28788
   452
  \cite{isabelle-sys} allows tagged command regions to be presented
wenzelm@27042
   453
  specifically, e.g.\ to fold proof texts, or drop parts of the text
wenzelm@27042
   454
  completely.
wenzelm@27042
   455
wenzelm@28788
   456
  For example ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharpercent}invisible\ auto{\isachardoublequote}}'' causes
wenzelm@28788
   457
  that piece of proof to be treated as \isa{invisible} instead of
wenzelm@28788
   458
  \isa{{\isachardoublequote}proof{\isachardoublequote}} (the default), which may be shown or hidden
wenzelm@28788
   459
  depending on the document setup.  In contrast, ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharpercent}visible\ auto{\isachardoublequote}}'' forces this text to be shown
wenzelm@27042
   460
  invariably.
wenzelm@27042
   461
wenzelm@27042
   462
  Explicit tag specifications within a proof apply to all subsequent
wenzelm@28788
   463
  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}}}}'' forces the whole
wenzelm@28788
   464
  sub-proof to be typeset as \isa{visible} (unless some of its parts
wenzelm@28788
   465
  are tagged differently).
wenzelm@28788
   466
wenzelm@28788
   467
  \medskip Command tags merely produce certain markup environments for
wenzelm@28788
   468
  type-setting.  The meaning of these is determined by {\LaTeX}
wenzelm@28788
   469
  macros, as defined in \hyperlink{file.~~/lib/texinputs/isabelle.sty}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}lib{\isacharslash}texinputs{\isacharslash}isabelle{\isachardot}sty}}}} or
wenzelm@28788
   470
  by the document author.  The Isabelle document preparation tools
wenzelm@28788
   471
  also provide some high-level options to specify the meaning of
wenzelm@28788
   472
  arbitrary tags to ``keep'', ``drop'', or ``fold'' the corresponding
wenzelm@28788
   473
  parts of the text.  Logic sessions may also specify ``document
wenzelm@28788
   474
  versions'', where given tags are interpreted in some particular way.
wenzelm@28788
   475
  Again see \cite{isabelle-sys} for further details.%
wenzelm@27042
   476
\end{isamarkuptext}%
wenzelm@27042
   477
\isamarkuptrue%
wenzelm@27042
   478
%
wenzelm@27042
   479
\isamarkupsection{Draft presentation%
wenzelm@27042
   480
}
wenzelm@27042
   481
\isamarkuptrue%
wenzelm@27042
   482
%
wenzelm@27042
   483
\begin{isamarkuptext}%
wenzelm@27042
   484
\begin{matharray}{rcl}
wenzelm@28788
   485
    \indexdef{}{command}{display\_drafts}\hypertarget{command.display-drafts}{\hyperlink{command.display-drafts}{\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
wenzelm@28788
   486
    \indexdef{}{command}{print\_drafts}\hypertarget{command.print-drafts}{\hyperlink{command.print-drafts}{\mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
wenzelm@27042
   487
  \end{matharray}
wenzelm@27042
   488
wenzelm@27042
   489
  \begin{rail}
wenzelm@40255
   490
    ('display_drafts' | 'print_drafts') (name +)
wenzelm@27042
   491
    ;
wenzelm@27042
   492
  \end{rail}
wenzelm@27042
   493
wenzelm@28788
   494
  \begin{description}
wenzelm@27042
   495
wenzelm@28788
   496
  \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
   497
  of raw source files.  Only those symbols that do not require
wenzelm@27042
   498
  additional {\LaTeX} packages are displayed properly, everything else
wenzelm@27042
   499
  is left verbatim.
wenzelm@27042
   500
wenzelm@28788
   501
  \end{description}%
wenzelm@27042
   502
\end{isamarkuptext}%
wenzelm@27042
   503
\isamarkuptrue%
wenzelm@27042
   504
%
wenzelm@27042
   505
\isadelimtheory
wenzelm@27042
   506
%
wenzelm@27042
   507
\endisadelimtheory
wenzelm@27042
   508
%
wenzelm@27042
   509
\isatagtheory
wenzelm@27042
   510
\isacommand{end}\isamarkupfalse%
wenzelm@27042
   511
%
wenzelm@27042
   512
\endisatagtheory
wenzelm@27042
   513
{\isafoldtheory}%
wenzelm@27042
   514
%
wenzelm@27042
   515
\isadelimtheory
wenzelm@27042
   516
%
wenzelm@27042
   517
\endisadelimtheory
wenzelm@27042
   518
\isanewline
wenzelm@27042
   519
\end{isabellebody}%
wenzelm@27042
   520
%%% Local Variables:
wenzelm@27042
   521
%%% mode: latex
wenzelm@27042
   522
%%% TeX-master: "root"
wenzelm@27042
   523
%%% End: