doc-src/IsarImplementation/Thy/prelim.thy
author wenzelm
Wed Aug 30 12:28:32 2006 +0200 (2006-08-30)
changeset 20437 0eb5e30fd620
parent 20430 fd646e926983
child 20447 5b75f1c4d7d6
permissions -rw-r--r--
tuned;
wenzelm@18537
     1
wenzelm@18537
     2
(* $Id$ *)
wenzelm@18537
     3
wenzelm@18537
     4
theory prelim imports base begin
wenzelm@18537
     5
wenzelm@18537
     6
chapter {* Preliminaries *}
wenzelm@18537
     7
wenzelm@20429
     8
section {* Contexts \label{sec:context} *}
wenzelm@18537
     9
wenzelm@20429
    10
text {*
wenzelm@20429
    11
  A logical context represents the background that is taken for
wenzelm@20429
    12
  granted when formulating statements and composing proofs.  It acts
wenzelm@20429
    13
  as a medium to produce formal content, depending on earlier material
wenzelm@20429
    14
  (declarations, results etc.).
wenzelm@18537
    15
wenzelm@20429
    16
  In particular, derivations within the primitive Pure logic can be
wenzelm@20429
    17
  described as a judgment @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}, meaning that a
wenzelm@20429
    18
  proposition @{text "\<phi>"} is derivable from hypotheses @{text "\<Gamma>"}
wenzelm@20429
    19
  within the theory @{text "\<Theta>"}.  There are logical reasons for
wenzelm@20429
    20
  keeping @{text "\<Theta>"} and @{text "\<Gamma>"} separate: theories support type
wenzelm@20429
    21
  constructors and schematic polymorphism of constants and axioms,
wenzelm@20429
    22
  while the inner calculus of @{text "\<Gamma> \<turnstile> \<phi>"} is limited to Simple
wenzelm@20429
    23
  Type Theory (with fixed type variables in the assumptions).
wenzelm@18537
    24
wenzelm@20429
    25
  \medskip Contexts and derivations are linked by the following key
wenzelm@20429
    26
  principles:
wenzelm@20429
    27
wenzelm@20429
    28
  \begin{itemize}
wenzelm@20429
    29
wenzelm@20429
    30
  \item Transfer: monotonicity of derivations admits results to be
wenzelm@20429
    31
  transferred into a larger context, i.e.\ @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}
wenzelm@20429
    32
  implies @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta>\<^sub>' \<phi>"} for contexts @{text "\<Theta>' \<supseteq>
wenzelm@20429
    33
  \<Theta>"} and @{text "\<Gamma>' \<supseteq> \<Gamma>"}.
wenzelm@18537
    34
wenzelm@20429
    35
  \item Export: discharge of hypotheses admits results to be exported
wenzelm@20429
    36
  into a smaller context, i.e.\ @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta> \<phi>"} implies
wenzelm@20429
    37
  @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<Delta> \<Longrightarrow> \<phi>"} where @{text "\<Gamma>' \<supseteq> \<Gamma>"} and @{text "\<Delta> =
wenzelm@20429
    38
  \<Gamma>' - \<Gamma>"}.  Note that @{text "\<Theta>"} remains unchanged here, only the
wenzelm@20429
    39
  @{text "\<Gamma>"} part is affected.
wenzelm@20429
    40
wenzelm@20429
    41
  \end{itemize}
wenzelm@18537
    42
wenzelm@20429
    43
  \medskip Isabelle/Isar provides two different notions of abstract
wenzelm@20429
    44
  containers called \emph{theory context} and \emph{proof context},
wenzelm@20429
    45
  respectively.  These model the main characteristics of the primitive
wenzelm@20429
    46
  @{text "\<Theta>"} and @{text "\<Gamma>"} above, without subscribing to any
wenzelm@20429
    47
  particular kind of content yet.  Instead, contexts merely impose a
wenzelm@20429
    48
  certain policy of managing arbitrary \emph{context data}.  The
wenzelm@20429
    49
  system provides strongly typed mechanisms to declare new kinds of
wenzelm@20429
    50
  data at compile time.
wenzelm@18537
    51
wenzelm@20429
    52
  Thus the internal bootstrap process of Isabelle/Pure eventually
wenzelm@20429
    53
  reaches a stage where certain data slots provide the logical content
wenzelm@20429
    54
  of @{text "\<Theta>"} and @{text "\<Gamma>"} sketched above, but this does not
wenzelm@20429
    55
  stop there!  Various additional data slots support all kinds of
wenzelm@20429
    56
  mechanisms that are not necessarily part of the core logic.
wenzelm@18537
    57
wenzelm@20429
    58
  For example, there would be data for canonical introduction and
wenzelm@20429
    59
  elimination rules for arbitrary operators (depending on the
wenzelm@20429
    60
  object-logic and application), which enables users to perform
wenzelm@20429
    61
  standard proof steps implicitly (cf.\ the @{text "rule"} method).
wenzelm@18537
    62
wenzelm@20429
    63
  Isabelle is able to bring forth more and more concepts successively.
wenzelm@20429
    64
  In particular, an object-logic like Isabelle/HOL continues the
wenzelm@20429
    65
  Isabelle/Pure setup by adding specific components for automated
wenzelm@20429
    66
  reasoning (classical reasoner, tableau prover, structured induction
wenzelm@20429
    67
  etc.) and derived specification mechanisms (inductive predicates,
wenzelm@20429
    68
  recursive functions etc.).  All of this is based on the generic data
wenzelm@20429
    69
  management by theory and proof contexts.
wenzelm@18537
    70
*}
wenzelm@18537
    71
wenzelm@18537
    72
wenzelm@18537
    73
subsection {* Theory context \label{sec:context-theory} *}
wenzelm@18537
    74
wenzelm@20429
    75
text {*
wenzelm@20429
    76
  Each theory is explicitly named and holds a unique identifier.
wenzelm@20429
    77
  There is a separate \emph{theory reference} for pointing backwards
wenzelm@20429
    78
  to the enclosing theory context of derived entities.  Theories are
wenzelm@20429
    79
  related by a (nominal) sub-theory relation, which corresponds to the
wenzelm@20429
    80
  canonical dependency graph: each theory is derived from a certain
wenzelm@20429
    81
  sub-graph of ancestor theories.  The @{text "merge"} of two theories
wenzelm@20429
    82
  refers to the least upper bound, which actually degenerates into
wenzelm@20429
    83
  absorption of one theory into the other, due to the nominal
wenzelm@20429
    84
  sub-theory relation this.
wenzelm@18537
    85
wenzelm@20429
    86
  The @{text "begin"} operation starts a new theory by importing
wenzelm@20429
    87
  several parent theories and entering a special @{text "draft"} mode,
wenzelm@20429
    88
  which is sustained until the final @{text "end"} operation.  A draft
wenzelm@20429
    89
  mode theory acts like a linear type, where updates invalidate
wenzelm@20429
    90
  earlier drafts, but theory reference values will be propagated
wenzelm@20429
    91
  automatically.  Thus derived entities that ``belong'' to a draft
wenzelm@20429
    92
  might be transferred spontaneously to a larger context.  An
wenzelm@20429
    93
  invalidated draft is called ``stale''.  The @{text "copy"} operation
wenzelm@20429
    94
  produces an auxiliary version with the same data content, but is
wenzelm@20429
    95
  unrelated to the original: updates of the copy do not affect the
wenzelm@20429
    96
  original, neither does the sub-theory relation hold.
wenzelm@20429
    97
wenzelm@20429
    98
  The example below shows a theory graph derived from @{text "Pure"}.
wenzelm@20429
    99
  Theory @{text "Length"} imports @{text "Nat"} and @{text "List"}.
wenzelm@20429
   100
  The linear draft mode is enabled during the ``@{text "\<dots>"}'' stage of
wenzelm@20429
   101
  the theory body.
wenzelm@20429
   102
wenzelm@20429
   103
  \bigskip
wenzelm@20429
   104
  \begin{tabular}{rcccl}
wenzelm@18537
   105
        &            & $Pure$ \\
wenzelm@18537
   106
        &            & $\downarrow$ \\
wenzelm@18537
   107
        &            & $FOL$ \\
wenzelm@18537
   108
        & $\swarrow$ &              & $\searrow$ & \\
wenzelm@18537
   109
  $Nat$ &            &              &            & $List$ \\
wenzelm@18537
   110
        & $\searrow$ &              & $\swarrow$ \\
wenzelm@18537
   111
        &            & $Length$ \\
wenzelm@18537
   112
        &            & \multicolumn{3}{l}{~~$\isarkeyword{imports}$} \\
wenzelm@18537
   113
        &            & \multicolumn{3}{l}{~~$\isarkeyword{begin}$} \\
wenzelm@18537
   114
        &            & $\vdots$~~ \\
wenzelm@18537
   115
        &            & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\
wenzelm@20429
   116
  \end{tabular}
wenzelm@20429
   117
wenzelm@20429
   118
  \medskip In practice, derived theory operations mostly operate
wenzelm@20429
   119
  drafts, namely the body of the current portion of theory that the
wenzelm@20429
   120
  user happens to be composing.
wenzelm@18537
   121
wenzelm@20429
   122
 \medskip There is also a builtin theory history mechanism that amends for
wenzelm@20429
   123
  the destructive behaviour of theory drafts.  The @{text
wenzelm@20429
   124
  "checkpoint"} operation produces an intermediate stepping stone that
wenzelm@20429
   125
  survives the next update unscathed: both the original and the
wenzelm@20429
   126
  changed theory remain valid and are related by the sub-theory
wenzelm@20429
   127
  relation.  This recovering of pure theory values comes at the cost
wenzelm@20429
   128
  of extra internal bookeeping.  The cumulative effect of
wenzelm@20429
   129
  checkpointing is purged by the @{text "finish"} operation.
wenzelm@18537
   130
wenzelm@20429
   131
  History operations are usually managed by the system, e.g.\ notably
wenzelm@20429
   132
  in the Isar transaction loop.
wenzelm@18537
   133
wenzelm@20429
   134
  \medskip
wenzelm@20429
   135
  FIXME theory data
wenzelm@18537
   136
*}
wenzelm@18537
   137
wenzelm@20430
   138
text %mlref {*
wenzelm@20430
   139
*}
wenzelm@20430
   140
wenzelm@18537
   141
wenzelm@18537
   142
subsection {* Proof context \label{sec:context-proof} *}
wenzelm@18537
   143
wenzelm@18537
   144
text {*
wenzelm@20429
   145
  A proof context is an arbitrary container that is initialized from a
wenzelm@20429
   146
  given theory.  The result contains a back-reference to the theory it
wenzelm@20429
   147
  belongs to, together with pure data.  No further bookkeeping is
wenzelm@20429
   148
  required here, thanks to the lack of destructive features.
wenzelm@20429
   149
wenzelm@20429
   150
  There is no restriction on producing proof contexts, although the
wenzelm@20429
   151
  usual discipline is to follow block structure as a mental model: a
wenzelm@20429
   152
  given context is extended consecutively, results are exported back
wenzelm@20429
   153
  into the original context.  In particular, the concept of Isar proof
wenzelm@20429
   154
  state models block-structured reasoning explicitly, using a stack of
wenzelm@20429
   155
  proof contexts.
wenzelm@20429
   156
wenzelm@20429
   157
  Due to the lack of identification and back-referencing, entities
wenzelm@20429
   158
  derived in a proof context need to record inherent logical
wenzelm@20429
   159
  requirements explicitly.  For example, hypotheses used in a
wenzelm@20429
   160
  derivation will be recorded separately within the sequent @{text "\<Gamma>
wenzelm@20429
   161
  \<turnstile> \<phi>"}, just to make double sure.  Results could leak into an alien
wenzelm@20429
   162
  proof context do to programming errors, but Isabelle/Isar
wenzelm@20429
   163
  occasionally includes extra validity checks at the end of a
wenzelm@20429
   164
  sub-proof.
wenzelm@20429
   165
wenzelm@20429
   166
  \medskip
wenzelm@20429
   167
  FIXME proof data
wenzelm@18537
   168
wenzelm@18537
   169
\glossary{Proof context}{The static context of a structured proof,
wenzelm@18537
   170
acts like a local ``theory'' of the current portion of Isar proof
wenzelm@18537
   171
text, generalizes the idea of local hypotheses @{text "\<Gamma>"} in
wenzelm@18537
   172
judgments @{text "\<Gamma> \<turnstile> \<phi>"} of natural deduction calculi.  There is a
wenzelm@18537
   173
generic notion of introducing and discharging hypotheses.  Arbritrary
wenzelm@18537
   174
auxiliary context data may be adjoined.}
wenzelm@18537
   175
wenzelm@18537
   176
*}
wenzelm@18537
   177
wenzelm@20430
   178
text %mlref {* FIXME *}
wenzelm@20430
   179
wenzelm@20429
   180
wenzelm@20429
   181
subsection {* Generic contexts *}
wenzelm@20429
   182
wenzelm@20430
   183
text FIXME
wenzelm@20430
   184
wenzelm@20430
   185
text %mlref {* FIXME *}
wenzelm@20430
   186
wenzelm@20437
   187
wenzelm@20437
   188
section {* Named entities *}
wenzelm@20437
   189
wenzelm@20437
   190
text {* Named entities of different kinds (logical constant, type,
wenzelm@20437
   191
type class, theorem, method etc.) live in separate name spaces.  It is
wenzelm@20437
   192
usually clear from the occurrence of a name which kind of entity it
wenzelm@20437
   193
refers to.  For example, proof method @{text "foo"} vs.\ theorem
wenzelm@20437
   194
@{text "foo"} vs.\ logical constant @{text "foo"} are easily
wenzelm@20437
   195
distinguished by means of the syntactic context.  A notable exception
wenzelm@20437
   196
are logical identifiers within a term (\secref{sec:terms}): constants,
wenzelm@20437
   197
fixed variables, and bound variables all share the same identifier
wenzelm@20437
   198
syntax, but are distinguished by their scope.
wenzelm@20437
   199
wenzelm@20437
   200
Each name space is organized as a collection of \emph{qualified
wenzelm@20437
   201
names}, which consist of a sequence of basic name components separated
wenzelm@20437
   202
by dots: @{text "Bar.bar.foo"}, @{text "Bar.foo"}, and @{text "foo"}
wenzelm@20437
   203
are examples for valid qualified names.  Name components are
wenzelm@20437
   204
subdivided into \emph{symbols}, which constitute the smallest textual
wenzelm@20437
   205
unit in Isabelle --- raw characters are normally not encountered
wenzelm@20437
   206
directly. *}
wenzelm@20437
   207
wenzelm@20437
   208
wenzelm@20437
   209
subsection {* Strings of symbols *}
wenzelm@20437
   210
wenzelm@20437
   211
text {* Isabelle strings consist of a sequence of
wenzelm@20437
   212
symbols\glossary{Symbol}{The smalles unit of text in Isabelle,
wenzelm@20437
   213
subsumes plain ASCII characters as well as an infinite collection of
wenzelm@20437
   214
named symbols (for greek, math etc.).}, which are either packed as an
wenzelm@20437
   215
actual @{text "string"}, or represented as a list.  Each symbol is in
wenzelm@20437
   216
itself a small string of the following form:
wenzelm@20437
   217
wenzelm@20437
   218
\begin{enumerate}
wenzelm@20437
   219
wenzelm@20437
   220
\item either a singleton ASCII character ``@{text "c"}'' (with
wenzelm@20437
   221
character code 0--127), for example ``\verb,a,'',
wenzelm@20437
   222
wenzelm@20437
   223
\item or a regular symbol ``\verb,\,\verb,<,@{text "ident"}\verb,>,'',
wenzelm@20437
   224
for example ``\verb,\,\verb,<alpha>,'',
wenzelm@20437
   225
wenzelm@20437
   226
\item or a control symbol ``\verb,\,\verb,<^,@{text
wenzelm@20437
   227
"ident"}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
wenzelm@20437
   228
wenzelm@20437
   229
\item or a raw control symbol ``\verb,\,\verb,<^raw:,@{text
wenzelm@20437
   230
"\<dots>"}\verb,>,'' where ``@{text "\<dots>"}'' refers to any
wenzelm@20437
   231
printable ASCII character (excluding ``\verb,.,'' and ``\verb,>,'') or
wenzelm@20437
   232
non-ASCII character, for example ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
wenzelm@20437
   233
wenzelm@20437
   234
\item or a numbered raw control symbol ``\verb,\,\verb,<^raw,@{text
wenzelm@20437
   235
"nnn"}\verb,>, where @{text "nnn"} are digits, for example
wenzelm@20437
   236
``\verb,\,\verb,<^raw42>,''.
wenzelm@20437
   237
wenzelm@20437
   238
\end{enumerate}
wenzelm@20437
   239
wenzelm@20437
   240
The @{text "ident"} syntax for symbol names is @{text "letter (letter
wenzelm@20437
   241
| digit)\<^sup>*"}, where @{text "letter = A..Za..Z"} and @{text
wenzelm@20437
   242
"digit = 0..9"}.  There are infinitely many regular symbols and
wenzelm@20437
   243
control symbols available, but a certain collection of standard
wenzelm@20437
   244
symbols is treated specifically.  For example,
wenzelm@20437
   245
``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
wenzelm@20437
   246
which means it may occur within regular Isabelle identifier syntax.
wenzelm@20437
   247
wenzelm@20437
   248
Output of symbols depends on the print mode (\secref{sec:print-mode}).
wenzelm@20437
   249
For example, the standard {\LaTeX} setup of the Isabelle document
wenzelm@20437
   250
preparation system would present ``\verb,\,\verb,<alpha>,'' as @{text
wenzelm@20437
   251
"\<alpha>"}, and ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as @{text
wenzelm@20437
   252
"\<^bold>\<alpha>"}.
wenzelm@20437
   253
wenzelm@20437
   254
\medskip It is important to note that the character set underlying
wenzelm@20437
   255
Isabelle symbols is plain 7-bit ASCII.  Since 8-bit characters are
wenzelm@20437
   256
passed through transparently, Isabelle may easily process actual
wenzelm@20437
   257
Unicode/UCS data (using the well-known UTF-8 encoding, for example).
wenzelm@20437
   258
Unicode provides its own collection of mathematical symbols, but there
wenzelm@20437
   259
is presently no link to Isabelle's named ones; both kinds of symbols
wenzelm@20437
   260
coexist independently. *}
wenzelm@20437
   261
wenzelm@20437
   262
text %mlref {*
wenzelm@20437
   263
  \begin{mldecls}
wenzelm@20437
   264
  @{index_ML_type "Symbol.symbol"} \\
wenzelm@20437
   265
  @{index_ML Symbol.explode: "string -> Symbol.symbol list"} \\
wenzelm@20437
   266
  @{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\
wenzelm@20437
   267
  @{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\
wenzelm@20437
   268
  @{index_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\
wenzelm@20437
   269
  @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\
wenzelm@20437
   270
  @{index_ML_type "Symbol.sym"} \\
wenzelm@20437
   271
  @{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\
wenzelm@20437
   272
  \end{mldecls}
wenzelm@20437
   273
wenzelm@20437
   274
  \begin{description}
wenzelm@20437
   275
wenzelm@20437
   276
  \item @{ML_type "Symbol.symbol"} represents Isabelle symbols; this type
wenzelm@20437
   277
  is merely an alias for @{ML_type "string"}, but emphasizes the
wenzelm@20437
   278
  specific format encountered here.
wenzelm@20437
   279
wenzelm@20437
   280
  \item @{ML "Symbol.explode"}~@{text "s"} produces an actual symbol
wenzelm@20437
   281
  list from the packed form usually encountered as user input.  This
wenzelm@20437
   282
  function replaces @{ML "String.explode"} for virtually all purposes
wenzelm@20437
   283
  of manipulating text in Isabelle!  Plain @{text "implode"} may be
wenzelm@20437
   284
  used for the reverse operation.
wenzelm@20437
   285
wenzelm@20437
   286
  \item @{ML "Symbol.is_letter"}, @{ML "Symbol.is_digit"}, @{ML
wenzelm@20437
   287
  "Symbol.is_quasi"}, @{ML "Symbol.is_blank"} classify certain symbols
wenzelm@20437
   288
  (both ASCII and several named ones) according to fixed syntactic
wenzelm@20437
   289
  convections of Isabelle, e.g.\ see \cite{isabelle-isar-ref}.
wenzelm@20437
   290
wenzelm@20437
   291
  \item @{ML_type "Symbol.sym"} is a concrete datatype that represents
wenzelm@20437
   292
  the different kinds of symbols explicitly as @{ML "Symbol.Char"},
wenzelm@20437
   293
  @{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, or @{ML "Symbol.Raw"}.
wenzelm@20437
   294
wenzelm@20437
   295
  \item @{ML "Symbol.decode"} converts the string representation of a
wenzelm@20437
   296
  symbol into the explicit datatype version.
wenzelm@20437
   297
wenzelm@20437
   298
  \end{description}
wenzelm@20437
   299
*}
wenzelm@20437
   300
wenzelm@20437
   301
wenzelm@20437
   302
subsection {* Qualified names and name spaces *}
wenzelm@20437
   303
wenzelm@20437
   304
text %FIXME {* Qualified names are constructed according to implicit naming
wenzelm@20437
   305
principles of the present context.
wenzelm@20437
   306
wenzelm@20437
   307
wenzelm@20437
   308
The last component is called \emph{base name}; the remaining prefix of
wenzelm@20437
   309
qualification may be empty.
wenzelm@20437
   310
wenzelm@20437
   311
Some practical conventions help to organize named entities more
wenzelm@20437
   312
systematically:
wenzelm@20437
   313
wenzelm@20437
   314
\begin{itemize}
wenzelm@20437
   315
wenzelm@20437
   316
\item Names are qualified first by the theory name, second by an
wenzelm@20437
   317
optional ``structure''.  For example, a constant @{text "c"} declared
wenzelm@20437
   318
as part of a certain structure @{text "b"} (say a type definition) in
wenzelm@20437
   319
theory @{text "A"} will be named @{text "A.b.c"} internally.
wenzelm@20437
   320
wenzelm@20437
   321
\item
wenzelm@20437
   322
wenzelm@20437
   323
\item
wenzelm@20437
   324
wenzelm@20437
   325
\item
wenzelm@20437
   326
wenzelm@20437
   327
\item
wenzelm@20437
   328
wenzelm@20437
   329
\end{itemize}
wenzelm@20437
   330
wenzelm@20437
   331
Names of different kinds of entities are basically independent, but
wenzelm@20437
   332
some practical naming conventions relate them to each other.  For
wenzelm@20437
   333
example, a constant @{text "foo"} may be accompanied with theorems
wenzelm@20437
   334
@{text "foo.intro"}, @{text "foo.elim"}, @{text "foo.simps"} etc.  The
wenzelm@20437
   335
same may happen for a type @{text "foo"}, which is then apt to cause
wenzelm@20437
   336
clashes in the theorem name space!  To avoid this, we occasionally
wenzelm@20437
   337
follow an additional convention of suffixes that determine the
wenzelm@20437
   338
original kind of entity that a name has been derived.  For example,
wenzelm@20437
   339
constant @{text "foo"} is associated with theorem @{text "foo.intro"},
wenzelm@20437
   340
type @{text "foo"} with theorem @{text "foo_type.intro"}, and type
wenzelm@20437
   341
class @{text "foo"} with @{text "foo_class.intro"}.
wenzelm@20437
   342
wenzelm@20437
   343
*}
wenzelm@20437
   344
wenzelm@20437
   345
wenzelm@20437
   346
section {* Structured output *}
wenzelm@20437
   347
wenzelm@20437
   348
subsection {* Pretty printing *}
wenzelm@20437
   349
wenzelm@20437
   350
text FIXME
wenzelm@20437
   351
wenzelm@20437
   352
subsection {* Output channels *}
wenzelm@20437
   353
wenzelm@20437
   354
text FIXME
wenzelm@20437
   355
wenzelm@20437
   356
subsection {* Print modes *}
wenzelm@20437
   357
wenzelm@20437
   358
text FIXME
wenzelm@20437
   359
wenzelm@20437
   360
wenzelm@18537
   361
end