doc-src/IsarRef/Thy/document/Document_Preparation.tex
author wenzelm
Sat Feb 28 17:09:32 2009 +0100 (2009-02-28)
changeset 30172 afdf7808cfd0
parent 28788 ff9d8a8932e4
child 30397 b6212ae21656
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
%
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@27052
   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} \\
wenzelm@28788
   162
    \indexdef{}{antiquotation}{const}\hypertarget{antiquotation.const}{\hyperlink{antiquotation.const}{\mbox{\isa{const}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   163
    \indexdef{}{antiquotation}{abbrev}\hypertarget{antiquotation.abbrev}{\hyperlink{antiquotation.abbrev}{\mbox{\isa{abbrev}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   164
    \indexdef{}{antiquotation}{typeof}\hypertarget{antiquotation.typeof}{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   165
    \indexdef{}{antiquotation}{typ}\hypertarget{antiquotation.typ}{\hyperlink{antiquotation.typ}{\mbox{\isa{typ}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   166
    \indexdef{}{antiquotation}{thm\_style}\hypertarget{antiquotation.thm-style}{\hyperlink{antiquotation.thm-style}{\mbox{\isa{thm{\isacharunderscore}style}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   167
    \indexdef{}{antiquotation}{term\_style}\hypertarget{antiquotation.term-style}{\hyperlink{antiquotation.term-style}{\mbox{\isa{term{\isacharunderscore}style}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   168
    \indexdef{}{antiquotation}{text}\hypertarget{antiquotation.text}{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   169
    \indexdef{}{antiquotation}{goals}\hypertarget{antiquotation.goals}{\hyperlink{antiquotation.goals}{\mbox{\isa{goals}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   170
    \indexdef{}{antiquotation}{subgoals}\hypertarget{antiquotation.subgoals}{\hyperlink{antiquotation.subgoals}{\mbox{\isa{subgoals}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   171
    \indexdef{}{antiquotation}{prf}\hypertarget{antiquotation.prf}{\hyperlink{antiquotation.prf}{\mbox{\isa{prf}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   172
    \indexdef{}{antiquotation}{full\_prf}\hypertarget{antiquotation.full-prf}{\hyperlink{antiquotation.full-prf}{\mbox{\isa{full{\isacharunderscore}prf}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   173
    \indexdef{}{antiquotation}{ML}\hypertarget{antiquotation.ML}{\hyperlink{antiquotation.ML}{\mbox{\isa{ML}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   174
    \indexdef{}{antiquotation}{ML\_type}\hypertarget{antiquotation.ML-type}{\hyperlink{antiquotation.ML-type}{\mbox{\isa{ML{\isacharunderscore}type}}}} & : & \isa{antiquotation} \\
wenzelm@28788
   175
    \indexdef{}{antiquotation}{ML\_struct}\hypertarget{antiquotation.ML-struct}{\hyperlink{antiquotation.ML-struct}{\mbox{\isa{ML{\isacharunderscore}struct}}}} & : & \isa{antiquotation} \\
wenzelm@27042
   176
  \end{matharray}
wenzelm@27042
   177
wenzelm@28788
   178
  The overall content of an Isabelle/Isar theory may alternate between
wenzelm@28788
   179
  formal and informal text.  The main body consists of formal
wenzelm@28788
   180
  specification and proof commands, interspersed with markup commands
wenzelm@28788
   181
  (\secref{sec:markup}) or document comments (\secref{sec:comments}).
wenzelm@28788
   182
  The argument of markup commands quotes informal text to be printed
wenzelm@28788
   183
  in the resulting document, but may again refer to formal entities
wenzelm@28788
   184
  via \emph{document antiquotations}.
wenzelm@27042
   185
wenzelm@28788
   186
  For example, embedding of ``\isa{{\isacharat}{\isacharbraceleft}term\ {\isacharbrackleft}show{\isacharunderscore}types{\isacharbrackright}\ {\isachardoublequote}f\ x\ {\isacharequal}\ a\ {\isacharplus}\ x{\isachardoublequote}{\isacharbraceright}}''
wenzelm@28788
   187
  within a text block makes
wenzelm@28788
   188
  \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
   189
wenzelm@28788
   190
  Antiquotations usually spare the author tedious typing of logical
wenzelm@28788
   191
  entities in full detail.  Even more importantly, some degree of
wenzelm@28788
   192
  consistency-checking between the main body of formal text and its
wenzelm@28788
   193
  informal explanation is achieved, since terms and types appearing in
wenzelm@28788
   194
  antiquotations are checked within the current theory or proof
wenzelm@28788
   195
  context.
wenzelm@27042
   196
wenzelm@27042
   197
  \begin{rail}
wenzelm@27042
   198
    atsign lbrace antiquotation rbrace
wenzelm@27042
   199
    ;
wenzelm@27042
   200
wenzelm@27042
   201
    antiquotation:
wenzelm@27042
   202
      'theory' options name |
wenzelm@27042
   203
      'thm' options thmrefs |
haftmann@27453
   204
      'lemma' options prop 'by' method |
wenzelm@27042
   205
      'prop' options prop |
wenzelm@27042
   206
      'term' options term |
wenzelm@27042
   207
      'const' options term |
wenzelm@27042
   208
      'abbrev' options term |
wenzelm@27042
   209
      'typeof' options term |
wenzelm@27042
   210
      'typ' options type |
wenzelm@27042
   211
      'thm\_style' options name thmref |
wenzelm@27042
   212
      'term\_style' options name term |
wenzelm@27042
   213
      'text' options name |
wenzelm@27042
   214
      'goals' options |
wenzelm@27042
   215
      'subgoals' options |
wenzelm@27042
   216
      'prf' options thmrefs |
wenzelm@27042
   217
      'full\_prf' options thmrefs |
wenzelm@27042
   218
      'ML' options name |
wenzelm@27042
   219
      'ML\_type' options name |
wenzelm@27042
   220
      'ML\_struct' options name
wenzelm@27042
   221
    ;
wenzelm@27042
   222
    options: '[' (option * ',') ']'
wenzelm@27042
   223
    ;
wenzelm@27042
   224
    option: name | name '=' name
wenzelm@27042
   225
    ;
wenzelm@27042
   226
  \end{rail}
wenzelm@27042
   227
wenzelm@27042
   228
  Note that the syntax of antiquotations may \emph{not} include source
wenzelm@28788
   229
  comments \verb|(*|~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\verb|*)| nor verbatim
wenzelm@27042
   230
  text \verb|{|\verb|*|~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\verb|*|\verb|}|.
wenzelm@27042
   231
wenzelm@28788
   232
  \begin{description}
wenzelm@27042
   233
  
wenzelm@28788
   234
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}theory\ A{\isacharbraceright}{\isachardoublequote}} prints the name \isa{{\isachardoublequote}A{\isachardoublequote}}, which is
wenzelm@27042
   235
  guaranteed to refer to a valid ancestor theory in the current
wenzelm@27042
   236
  context.
wenzelm@27042
   237
wenzelm@28788
   238
  \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
   239
  Full fact expressions are allowed here, including attributes
wenzelm@28788
   240
  (\secref{sec:syn-att}).
wenzelm@28788
   241
wenzelm@28788
   242
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prop\ {\isasymphi}{\isacharbraceright}{\isachardoublequote}} prints a well-typed proposition \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}.
wenzelm@27042
   243
wenzelm@28788
   244
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}lemma\ {\isasymphi}\ by\ m{\isacharbraceright}{\isachardoublequote}} proves a well-typed proposition
wenzelm@28788
   245
  \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}} by method \isa{m} and prints the original \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}.
haftmann@27453
   246
wenzelm@28788
   247
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ t{\isacharbraceright}{\isachardoublequote}} prints a well-typed term \isa{{\isachardoublequote}t{\isachardoublequote}}.
wenzelm@27042
   248
wenzelm@28788
   249
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}const\ c{\isacharbraceright}{\isachardoublequote}} prints a logical or syntactic constant
wenzelm@27042
   250
  \isa{{\isachardoublequote}c{\isachardoublequote}}.
wenzelm@27042
   251
  
wenzelm@28788
   252
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}abbrev\ c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isacharbraceright}{\isachardoublequote}} prints a constant abbreviation
wenzelm@28788
   253
  \isa{{\isachardoublequote}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ rhs{\isachardoublequote}} as defined in the current context.
wenzelm@27042
   254
wenzelm@28788
   255
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typeof\ t{\isacharbraceright}{\isachardoublequote}} prints the type of a well-typed term
wenzelm@27042
   256
  \isa{{\isachardoublequote}t{\isachardoublequote}}.
wenzelm@27042
   257
wenzelm@28788
   258
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typ\ {\isasymtau}{\isacharbraceright}{\isachardoublequote}} prints a well-formed type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}.
wenzelm@27042
   259
  
wenzelm@28788
   260
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm{\isacharunderscore}style\ s\ a{\isacharbraceright}{\isachardoublequote}} prints theorem \isa{a},
wenzelm@27042
   261
  previously applying a style \isa{s} to it (see below).
wenzelm@27042
   262
  
wenzelm@28788
   263
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term{\isacharunderscore}style\ s\ t{\isacharbraceright}{\isachardoublequote}} prints a well-typed term \isa{t}
wenzelm@28788
   264
  after applying a style \isa{s} to it (see below).
wenzelm@27042
   265
wenzelm@28788
   266
  \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
   267
  to the Isabelle document style, without demanding well-formedness,
wenzelm@28788
   268
  e.g.\ small pieces of terms that should not be parsed or
wenzelm@28788
   269
  type-checked yet.
wenzelm@27042
   270
wenzelm@28788
   271
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}goals{\isacharbraceright}{\isachardoublequote}} prints the current \emph{dynamic} goal
wenzelm@27042
   272
  state.  This is mainly for support of tactic-emulation scripts
wenzelm@28788
   273
  within Isar.  Presentation of goal states does not conform to the
wenzelm@28788
   274
  idea of human-readable proof documents!
wenzelm@27042
   275
wenzelm@28788
   276
  When explaining proofs in detail it is usually better to spell out
wenzelm@28788
   277
  the reasoning via proper Isar proof commands, instead of peeking at
wenzelm@28788
   278
  the internal machine configuration.
wenzelm@27042
   279
  
wenzelm@28788
   280
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}subgoals{\isacharbraceright}{\isachardoublequote}} is similar to \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}goals{\isacharbraceright}{\isachardoublequote}}, but
wenzelm@27042
   281
  does not print the main goal.
wenzelm@27042
   282
  
wenzelm@28788
   283
  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}} prints the (compact) proof terms
wenzelm@28788
   284
  corresponding to the theorems \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}. Note that this
wenzelm@28788
   285
  requires proof terms to be switched on for the current logic
wenzelm@28788
   286
  session.
wenzelm@27042
   287
  
wenzelm@28788
   288
  \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
   289
  information omitted in the compact proof term, which is denoted by
wenzelm@28788
   290
  ``\isa{{\isacharunderscore}}'' placeholders there.
wenzelm@27042
   291
  
wenzelm@28788
   292
  \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
   293
  structure, respectively.  The source is printed verbatim.
wenzelm@27042
   294
wenzelm@28788
   295
  \end{description}%
wenzelm@28788
   296
\end{isamarkuptext}%
wenzelm@28788
   297
\isamarkuptrue%
wenzelm@28788
   298
%
wenzelm@28788
   299
\isamarkupsubsubsection{Styled antiquotations%
wenzelm@28788
   300
}
wenzelm@28788
   301
\isamarkuptrue%
wenzelm@28788
   302
%
wenzelm@28788
   303
\begin{isamarkuptext}%
wenzelm@28788
   304
Some antiquotations like \isa{thm{\isacharunderscore}style} and \isa{term{\isacharunderscore}style} admit an extra \emph{style} specification to modify the
wenzelm@28788
   305
  printed result.  The following standard styles are available:
wenzelm@27042
   306
wenzelm@28788
   307
  \begin{description}
wenzelm@27042
   308
  
wenzelm@28788
   309
  \item \isa{lhs} extracts the first argument of any application
wenzelm@28788
   310
  form with at least two arguments --- typically meta-level or
wenzelm@27042
   311
  object-level equality, or any other binary relation.
wenzelm@27042
   312
  
wenzelm@28788
   313
  \item \isa{rhs} is like \isa{lhs}, but extracts the second
wenzelm@27042
   314
  argument.
wenzelm@27042
   315
  
wenzelm@28788
   316
  \item \isa{{\isachardoublequote}concl{\isachardoublequote}} extracts the conclusion \isa{C} from a rule
wenzelm@27042
   317
  in Horn-clause normal form \isa{{\isachardoublequote}A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C{\isachardoublequote}}.
wenzelm@27042
   318
  
wenzelm@28788
   319
  \item \isa{{\isachardoublequote}prem{\isadigit{1}}{\isachardoublequote}}, \dots, \isa{{\isachardoublequote}prem{\isadigit{9}}{\isachardoublequote}} extract premise number
wenzelm@28788
   320
  \isa{{\isachardoublequote}{\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isadigit{9}}{\isachardoublequote}}, respectively, from from a rule in Horn-clause
wenzelm@28788
   321
  normal form \isa{{\isachardoublequote}A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C{\isachardoublequote}}
wenzelm@27042
   322
wenzelm@28788
   323
  \end{description}%
wenzelm@28788
   324
\end{isamarkuptext}%
wenzelm@28788
   325
\isamarkuptrue%
wenzelm@28788
   326
%
wenzelm@28788
   327
\isamarkupsubsubsection{General options%
wenzelm@28788
   328
}
wenzelm@28788
   329
\isamarkuptrue%
wenzelm@28788
   330
%
wenzelm@28788
   331
\begin{isamarkuptext}%
wenzelm@28788
   332
The following options are available to tune the printed output
wenzelm@28788
   333
  of antiquotations.  Note that many of these coincide with global ML
wenzelm@28788
   334
  flags of the same names.
wenzelm@27042
   335
wenzelm@28788
   336
  \begin{description}
wenzelm@27042
   337
wenzelm@28788
   338
  \item \isa{{\isachardoublequote}show{\isacharunderscore}types\ {\isacharequal}\ bool{\isachardoublequote}} and \isa{{\isachardoublequote}show{\isacharunderscore}sorts\ {\isacharequal}\ bool{\isachardoublequote}}
wenzelm@27042
   339
  control printing of explicit type and sort constraints.
wenzelm@27042
   340
wenzelm@28788
   341
  \item \isa{{\isachardoublequote}show{\isacharunderscore}structs\ {\isacharequal}\ bool{\isachardoublequote}} controls printing of implicit
wenzelm@27042
   342
  structures.
wenzelm@27042
   343
wenzelm@28788
   344
  \item \isa{{\isachardoublequote}long{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}} forces names of types and
wenzelm@27042
   345
  constants etc.\ to be printed in their fully qualified internal
wenzelm@27042
   346
  form.
wenzelm@27042
   347
wenzelm@28788
   348
  \item \isa{{\isachardoublequote}short{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}} forces names of types and
wenzelm@27042
   349
  constants etc.\ to be printed unqualified.  Note that internalizing
wenzelm@27042
   350
  the output again in the current context may well yield a different
wenzelm@27042
   351
  result.
wenzelm@27042
   352
wenzelm@28788
   353
  \item \isa{{\isachardoublequote}unique{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}} determines whether the printed
wenzelm@27042
   354
  version of qualified names should be made sufficiently long to avoid
wenzelm@27042
   355
  overlap with names declared further back.  Set to \isa{false} for
wenzelm@27042
   356
  more concise output.
wenzelm@27042
   357
wenzelm@28788
   358
  \item \isa{{\isachardoublequote}eta{\isacharunderscore}contract\ {\isacharequal}\ bool{\isachardoublequote}} prints terms in \isa{{\isasymeta}}-contracted form.
wenzelm@27042
   359
wenzelm@28788
   360
  \item \isa{{\isachardoublequote}display\ {\isacharequal}\ bool{\isachardoublequote}} indicates if the text is to be output
wenzelm@28788
   361
  as multi-line ``display material'', rather than a small piece of
wenzelm@28788
   362
  text without line breaks (which is the default).
wenzelm@27042
   363
wenzelm@28788
   364
  In this mode the embedded entities are printed in the same style as
wenzelm@28788
   365
  the main theory text.
wenzelm@28788
   366
wenzelm@28788
   367
  \item \isa{{\isachardoublequote}break\ {\isacharequal}\ bool{\isachardoublequote}} controls line breaks in non-display
wenzelm@27042
   368
  material.
wenzelm@27042
   369
wenzelm@28788
   370
  \item \isa{{\isachardoublequote}quotes\ {\isacharequal}\ bool{\isachardoublequote}} indicates if the output should be
wenzelm@27042
   371
  enclosed in double quotes.
wenzelm@27042
   372
wenzelm@28788
   373
  \item \isa{{\isachardoublequote}mode\ {\isacharequal}\ name{\isachardoublequote}} adds \isa{name} to the print mode to
wenzelm@27042
   374
  be used for presentation (see also \cite{isabelle-ref}).  Note that
wenzelm@27042
   375
  the standard setup for {\LaTeX} output is already present by
wenzelm@27042
   376
  default, including the modes \isa{latex} and \isa{xsymbols}.
wenzelm@27042
   377
wenzelm@28788
   378
  \item \isa{{\isachardoublequote}margin\ {\isacharequal}\ nat{\isachardoublequote}} and \isa{{\isachardoublequote}indent\ {\isacharequal}\ nat{\isachardoublequote}} change the
wenzelm@27042
   379
  margin or indentation for pretty printing of display material.
wenzelm@27042
   380
wenzelm@28788
   381
  \item \isa{{\isachardoublequote}goals{\isacharunderscore}limit\ {\isacharequal}\ nat{\isachardoublequote}} determines the maximum number of
wenzelm@28788
   382
  goals to be printed (for goal-based antiquotation).
wenzelm@27042
   383
wenzelm@28788
   384
  \item \isa{{\isachardoublequote}locale\ {\isacharequal}\ name{\isachardoublequote}} specifies an alternative locale
wenzelm@27042
   385
  context used for evaluating and printing the subsequent argument.
wenzelm@27042
   386
wenzelm@28788
   387
  \item \isa{{\isachardoublequote}source\ {\isacharequal}\ bool{\isachardoublequote}} prints the original source text of the
wenzelm@28788
   388
  antiquotation arguments, rather than its internal representation.
wenzelm@28788
   389
  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
   390
  antiquotation for unchecked output.
wenzelm@28788
   391
wenzelm@28788
   392
  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
   393
  to an internalized logical entity back to a source form, according
wenzelm@28788
   394
  to the syntax of the current context.  Thus the printed output is
wenzelm@28788
   395
  not under direct control of the author, it may even fluctuate a bit
wenzelm@28788
   396
  as the underlying theory is changed later on.
wenzelm@28788
   397
wenzelm@28788
   398
  In contrast, \isa{{\isachardoublequote}source\ {\isacharequal}\ true{\isachardoublequote}} admits direct printing of the
wenzelm@28788
   399
  given source text, with the desirable well-formedness check in the
wenzelm@28788
   400
  background, but without modification of the printed text.
wenzelm@28788
   401
wenzelm@28788
   402
  \end{description}
wenzelm@27042
   403
wenzelm@27042
   404
  For boolean flags, ``\isa{{\isachardoublequote}name\ {\isacharequal}\ true{\isachardoublequote}}'' may be abbreviated as
wenzelm@27042
   405
  ``\isa{name}''.  All of the above flags are disabled by default,
wenzelm@28788
   406
  unless changed from ML, say in the \verb|ROOT.ML| of the
wenzelm@28788
   407
  logic session.%
wenzelm@27042
   408
\end{isamarkuptext}%
wenzelm@27042
   409
\isamarkuptrue%
wenzelm@27042
   410
%
wenzelm@28788
   411
\isamarkupsection{Markup via command tags \label{sec:tags}%
wenzelm@27042
   412
}
wenzelm@27042
   413
\isamarkuptrue%
wenzelm@27042
   414
%
wenzelm@27042
   415
\begin{isamarkuptext}%
wenzelm@28788
   416
Each Isabelle/Isar command may be decorated by additional
wenzelm@28788
   417
  presentation tags, to indicate some modification in the way it is
wenzelm@28788
   418
  printed in the document.
wenzelm@27042
   419
wenzelm@27042
   420
  \indexouternonterm{tags}
wenzelm@27042
   421
  \begin{rail}
wenzelm@27042
   422
    tags: ( tag * )
wenzelm@27042
   423
    ;
wenzelm@27042
   424
    tag: '\%' (ident | string)
wenzelm@27042
   425
  \end{rail}
wenzelm@27042
   426
wenzelm@28788
   427
  Some tags are pre-declared for certain classes of commands, serving
wenzelm@28788
   428
  as default markup if no tags are given in the text:
wenzelm@27042
   429
wenzelm@28788
   430
  \medskip
wenzelm@27042
   431
  \begin{tabular}{ll}
wenzelm@27042
   432
    \isa{{\isachardoublequote}theory{\isachardoublequote}} & theory begin/end \\
wenzelm@27042
   433
    \isa{{\isachardoublequote}proof{\isachardoublequote}} & all proof commands \\
wenzelm@27042
   434
    \isa{{\isachardoublequote}ML{\isachardoublequote}} & all commands involving ML code \\
wenzelm@27042
   435
  \end{tabular}
wenzelm@27042
   436
wenzelm@28788
   437
  \medskip The Isabelle document preparation system
wenzelm@28788
   438
  \cite{isabelle-sys} allows tagged command regions to be presented
wenzelm@27042
   439
  specifically, e.g.\ to fold proof texts, or drop parts of the text
wenzelm@27042
   440
  completely.
wenzelm@27042
   441
wenzelm@28788
   442
  For example ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharpercent}invisible\ auto{\isachardoublequote}}'' causes
wenzelm@28788
   443
  that piece of proof to be treated as \isa{invisible} instead of
wenzelm@28788
   444
  \isa{{\isachardoublequote}proof{\isachardoublequote}} (the default), which may be shown or hidden
wenzelm@28788
   445
  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
   446
  invariably.
wenzelm@27042
   447
wenzelm@27042
   448
  Explicit tag specifications within a proof apply to all subsequent
wenzelm@28788
   449
  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
   450
  sub-proof to be typeset as \isa{visible} (unless some of its parts
wenzelm@28788
   451
  are tagged differently).
wenzelm@28788
   452
wenzelm@28788
   453
  \medskip Command tags merely produce certain markup environments for
wenzelm@28788
   454
  type-setting.  The meaning of these is determined by {\LaTeX}
wenzelm@28788
   455
  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
   456
  by the document author.  The Isabelle document preparation tools
wenzelm@28788
   457
  also provide some high-level options to specify the meaning of
wenzelm@28788
   458
  arbitrary tags to ``keep'', ``drop'', or ``fold'' the corresponding
wenzelm@28788
   459
  parts of the text.  Logic sessions may also specify ``document
wenzelm@28788
   460
  versions'', where given tags are interpreted in some particular way.
wenzelm@28788
   461
  Again see \cite{isabelle-sys} for further details.%
wenzelm@27042
   462
\end{isamarkuptext}%
wenzelm@27042
   463
\isamarkuptrue%
wenzelm@27042
   464
%
wenzelm@27042
   465
\isamarkupsection{Draft presentation%
wenzelm@27042
   466
}
wenzelm@27042
   467
\isamarkuptrue%
wenzelm@27042
   468
%
wenzelm@27042
   469
\begin{isamarkuptext}%
wenzelm@27042
   470
\begin{matharray}{rcl}
wenzelm@28788
   471
    \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
   472
    \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
   473
  \end{matharray}
wenzelm@27042
   474
wenzelm@27042
   475
  \begin{rail}
wenzelm@27042
   476
    ('display\_drafts' | 'print\_drafts') (name +)
wenzelm@27042
   477
    ;
wenzelm@27042
   478
  \end{rail}
wenzelm@27042
   479
wenzelm@28788
   480
  \begin{description}
wenzelm@27042
   481
wenzelm@28788
   482
  \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
   483
  of raw source files.  Only those symbols that do not require
wenzelm@27042
   484
  additional {\LaTeX} packages are displayed properly, everything else
wenzelm@27042
   485
  is left verbatim.
wenzelm@27042
   486
wenzelm@28788
   487
  \end{description}%
wenzelm@27042
   488
\end{isamarkuptext}%
wenzelm@27042
   489
\isamarkuptrue%
wenzelm@27042
   490
%
wenzelm@27042
   491
\isadelimtheory
wenzelm@27042
   492
%
wenzelm@27042
   493
\endisadelimtheory
wenzelm@27042
   494
%
wenzelm@27042
   495
\isatagtheory
wenzelm@27042
   496
\isacommand{end}\isamarkupfalse%
wenzelm@27042
   497
%
wenzelm@27042
   498
\endisatagtheory
wenzelm@27042
   499
{\isafoldtheory}%
wenzelm@27042
   500
%
wenzelm@27042
   501
\isadelimtheory
wenzelm@27042
   502
%
wenzelm@27042
   503
\endisadelimtheory
wenzelm@27042
   504
\isanewline
wenzelm@27042
   505
\end{isabellebody}%
wenzelm@27042
   506
%%% Local Variables:
wenzelm@27042
   507
%%% mode: latex
wenzelm@27042
   508
%%% TeX-master: "root"
wenzelm@27042
   509
%%% End: