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