src/Doc/IsarImplementation/Local_Theory.thy
author wenzelm
Sat, 05 Apr 2014 15:03:40 +0200
changeset 56421 1ffd7eaa778b
parent 52422 93f3f9a2ae91
permissions -rw-r--r--
updated to jedit_build-20140405: Code2HTML.jar, CommonControls.jar, Console.jar, kappalayout.jar, Navigator.jar, SideKick.jar, doc with jEdit manuals (ant dist-manuals);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29755
d66b34e46bdf observe usual theory naming conventions;
wenzelm
parents: 20520
diff changeset
     1
theory Local_Theory
d66b34e46bdf observe usual theory naming conventions;
wenzelm
parents: 20520
diff changeset
     2
imports Base
d66b34e46bdf observe usual theory naming conventions;
wenzelm
parents: 20520
diff changeset
     3
begin
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     4
34927
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 33834
diff changeset
     5
chapter {* Local theory specifications \label{ch:local-theory} *}
29759
bcb79ddf57da removed rudiments of glossary;
wenzelm
parents: 29755
diff changeset
     6
29764
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
     7
text {*
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
     8
  A \emph{local theory} combines aspects of both theory and proof
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
     9
  context (cf.\ \secref{sec:context}), such that definitional
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    10
  specifications may be given relatively to parameters and
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    11
  assumptions.  A local theory is represented as a regular proof
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    12
  context, augmented by administrative data about the \emph{target
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    13
  context}.
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    14
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    15
  The target is usually derived from the background theory by adding
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    16
  local @{text "\<FIX>"} and @{text "\<ASSUME>"} elements, plus
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    17
  suitable modifications of non-logical context data (e.g.\ a special
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    18
  type-checking discipline).  Once initialized, the target is ready to
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    19
  absorb definitional primitives: @{text "\<DEFINE>"} for terms and
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    20
  @{text "\<NOTE>"} for theorems.  Such definitions may get
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    21
  transformed in a target-specific way, but the programming interface
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    22
  hides such details.
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    23
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    24
  Isabelle/Pure provides target mechanisms for locales, type-classes,
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    25
  type-class instantiations, and general overloading.  In principle,
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    26
  users can implement new targets as well, but this rather arcane
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    27
  discipline is beyond the scope of this manual.  In contrast,
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    28
  implementing derived definitional packages to be used within a local
29765
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
    29
  theory context is quite easy: the interfaces are even simpler and
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
    30
  more abstract than the underlying primitives for raw theories.
29764
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    31
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    32
  Many definitional packages for local theories are available in
29765
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
    33
  Isabelle.  Although a few old packages only work for global
39839
08f59175e541 misc tuning;
wenzelm
parents: 38466
diff changeset
    34
  theories, the standard way of implementing definitional packages in
08f59175e541 misc tuning;
wenzelm
parents: 38466
diff changeset
    35
  Isabelle is via the local theory interface.
29764
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    36
*}
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    37
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    38
29759
bcb79ddf57da removed rudiments of glossary;
wenzelm
parents: 29755
diff changeset
    39
section {* Definitional elements *}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    40
29759
bcb79ddf57da removed rudiments of glossary;
wenzelm
parents: 29755
diff changeset
    41
text {*
29765
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
    42
  There are separate elements @{text "\<DEFINE> c \<equiv> t"} for terms, and
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
    43
  @{text "\<NOTE> b = thm"} for theorems.  Types are treated
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
    44
  implicitly, according to Hindley-Milner discipline (cf.\
29764
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    45
  \secref{sec:variables}).  These definitional primitives essentially
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    46
  act like @{text "let"}-bindings within a local context that may
29765
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
    47
  already contain earlier @{text "let"}-bindings and some initial
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
    48
  @{text "\<lambda>"}-bindings.  Thus we gain \emph{dependent definitions}
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
    49
  that are relative to an initial axiomatic context.  The following
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
    50
  diagram illustrates this idea of axiomatic elements versus
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
    51
  definitional elements:
29764
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    52
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    53
  \begin{center}
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    54
  \begin{tabular}{|l|l|l|}
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    55
  \hline
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    56
  & @{text "\<lambda>"}-binding & @{text "let"}-binding \\
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    57
  \hline
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    58
  types & fixed @{text "\<alpha>"} & arbitrary @{text "\<beta>"} \\
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    59
  terms & @{text "\<FIX> x :: \<tau>"} & @{text "\<DEFINE> c \<equiv> t"} \\
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    60
  theorems & @{text "\<ASSUME> a: A"} & @{text "\<NOTE> b = \<^BG>B\<^EN>"} \\
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    61
  \hline
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    62
  \end{tabular}
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    63
  \end{center}
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    64
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    65
  A user package merely needs to produce suitable @{text "\<DEFINE>"}
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    66
  and @{text "\<NOTE>"} elements according to the application.  For
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    67
  example, a package for inductive definitions might first @{text
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    68
  "\<DEFINE>"} a certain predicate as some fixed-point construction,
29765
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
    69
  then @{text "\<NOTE>"} a proven result about monotonicity of the
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
    70
  functor involved here, and then produce further derived concepts via
29764
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    71
  additional @{text "\<DEFINE>"} and @{text "\<NOTE>"} elements.
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    72
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    73
  The cumulative sequence of @{text "\<DEFINE>"} and @{text "\<NOTE>"}
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    74
  produced at package runtime is managed by the local theory
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    75
  infrastructure by means of an \emph{auxiliary context}.  Thus the
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    76
  system holds up the impression of working within a fully abstract
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    77
  situation with hypothetical entities: @{text "\<DEFINE> c \<equiv> t"}
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    78
  always results in a literal fact @{text "\<^BG>c \<equiv> t\<^EN>"}, where
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    79
  @{text "c"} is a fixed variable @{text "c"}.  The details about
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    80
  global constants, name spaces etc. are handled internally.
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    81
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    82
  So the general structure of a local theory is a sandwich of three
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    83
  layers:
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    84
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    85
  \begin{center}
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    86
  \framebox{\quad auxiliary context \quad\framebox{\quad target context \quad\framebox{\quad background theory\quad}}}
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    87
  \end{center}
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    88
39861
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39849
diff changeset
    89
  When a definitional package is finished, the auxiliary context is
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39849
diff changeset
    90
  reset to the target context.  The target now holds definitions for
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39849
diff changeset
    91
  terms and theorems that stem from the hypothetical @{text
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39849
diff changeset
    92
  "\<DEFINE>"} and @{text "\<NOTE>"} elements, transformed by the
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39849
diff changeset
    93
  particular target policy (see \cite[\S4--5]{Haftmann-Wenzel:2009}
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39849
diff changeset
    94
  for details).  *}
29764
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    95
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    96
text %mlref {*
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
    97
  \begin{mldecls}
29765
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
    98
  @{index_ML_type local_theory: Proof.context} \\
41621
55b16bd82142 updated Named_Target.init;
wenzelm
parents: 39877
diff changeset
    99
  @{index_ML Named_Target.init: "(local_theory -> local_theory) ->
55b16bd82142 updated Named_Target.init;
wenzelm
parents: 39877
diff changeset
   100
    string -> theory -> local_theory"} \\[1ex]
33834
7c06e19f717c adapted local theory operations -- eliminated odd kind;
wenzelm
parents: 33672
diff changeset
   101
  @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) ->
7c06e19f717c adapted local theory operations -- eliminated odd kind;
wenzelm
parents: 33672
diff changeset
   102
    local_theory -> (term * (string * thm)) * local_theory"} \\
33672
8bde36ec8eb1 updated Local_Theory and Theory_Target;
wenzelm
parents: 30272
diff changeset
   103
  @{index_ML Local_Theory.note: "Attrib.binding * thm list ->
8bde36ec8eb1 updated Local_Theory and Theory_Target;
wenzelm
parents: 30272
diff changeset
   104
    local_theory -> (string * thm list) * local_theory"} \\
29764
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
   105
  \end{mldecls}
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
   106
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
   107
  \begin{description}
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
   108
39864
wenzelm
parents: 39861
diff changeset
   109
  \item Type @{ML_type local_theory} represents local theories.
wenzelm
parents: 39861
diff changeset
   110
  Although this is merely an alias for @{ML_type Proof.context}, it is
29765
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   111
  semantically a subtype of the same: a @{ML_type local_theory} holds
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   112
  target information as special context data.  Subtyping means that
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   113
  any value @{text "lthy:"}~@{ML_type local_theory} can be also used
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   114
  with operations on expecting a regular @{text "ctxt:"}~@{ML_type
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   115
  Proof.context}.
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   116
41621
55b16bd82142 updated Named_Target.init;
wenzelm
parents: 39877
diff changeset
   117
  \item @{ML Named_Target.init}~@{text "before_exit name thy"}
55b16bd82142 updated Named_Target.init;
wenzelm
parents: 39877
diff changeset
   118
  initializes a local theory derived from the given background theory.
55b16bd82142 updated Named_Target.init;
wenzelm
parents: 39877
diff changeset
   119
  An empty name refers to a \emph{global theory} context, and a
55b16bd82142 updated Named_Target.init;
wenzelm
parents: 39877
diff changeset
   120
  non-empty name refers to a @{command locale} or @{command class}
55b16bd82142 updated Named_Target.init;
wenzelm
parents: 39877
diff changeset
   121
  context (a fully-qualified internal name is expected here).  This is
55b16bd82142 updated Named_Target.init;
wenzelm
parents: 39877
diff changeset
   122
  useful for experimentation --- normally the Isar toplevel already
55b16bd82142 updated Named_Target.init;
wenzelm
parents: 39877
diff changeset
   123
  takes care to initialize the local theory context.  The given @{text
55b16bd82142 updated Named_Target.init;
wenzelm
parents: 39877
diff changeset
   124
  "before_exit"} function is invoked before leaving the context; in
55b16bd82142 updated Named_Target.init;
wenzelm
parents: 39877
diff changeset
   125
  most situations plain identity @{ML I} is sufficient.
29764
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
   126
33834
7c06e19f717c adapted local theory operations -- eliminated odd kind;
wenzelm
parents: 33672
diff changeset
   127
  \item @{ML Local_Theory.define}~@{text "((b, mx), (a, rhs))
29765
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   128
  lthy"} defines a local entity according to the specification that is
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   129
  given relatively to the current @{text "lthy"} context.  In
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   130
  particular the term of the RHS may refer to earlier local entities
29766
wenzelm
parents: 29765
diff changeset
   131
  from the auxiliary context, or hypothetical parameters from the
29765
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   132
  target context.  The result is the newly defined term (which is
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   133
  always a fixed variable with exactly the same name as specified for
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   134
  the LHS), together with an equational theorem that states the
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   135
  definition as a hypothetical fact.
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   136
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   137
  Unless an explicit name binding is given for the RHS, the resulting
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   138
  fact will be called @{text "b_def"}.  Any given attributes are
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   139
  applied to that same fact --- immediately in the auxiliary context
29766
wenzelm
parents: 29765
diff changeset
   140
  \emph{and} in any transformed versions stemming from target-specific
29765
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   141
  policies or any later interpretations of results from the target
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   142
  context (think of @{command locale} and @{command interpretation},
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   143
  for example).  This means that attributes should be usually plain
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   144
  declarations such as @{attribute simp}, while non-trivial rules like
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   145
  @{attribute simplified} are better avoided.
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   146
33672
8bde36ec8eb1 updated Local_Theory and Theory_Target;
wenzelm
parents: 30272
diff changeset
   147
  \item @{ML Local_Theory.note}~@{text "(a, ths) lthy"} is
8bde36ec8eb1 updated Local_Theory and Theory_Target;
wenzelm
parents: 30272
diff changeset
   148
  analogous to @{ML Local_Theory.define}, but defines facts instead of
29765
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   149
  terms.  There is also a slightly more general variant @{ML
33672
8bde36ec8eb1 updated Local_Theory and Theory_Target;
wenzelm
parents: 30272
diff changeset
   150
  Local_Theory.notes} that defines several facts (with attribute
29765
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   151
  expressions) simultaneously.
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   152
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   153
  This is essentially the internal version of the @{command lemmas}
9930a0d8dd32 more on local theories;
wenzelm
parents: 29764
diff changeset
   154
  command, or @{command declare} if an empty name binding is given.
29764
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
   155
b0b6d34388e9 some text on local theory specifications;
wenzelm
parents: 29759
diff changeset
   156
  \end{description}
29759
bcb79ddf57da removed rudiments of glossary;
wenzelm
parents: 29755
diff changeset
   157
*}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   158
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 18537
diff changeset
   159
39849
b7b1a9e8f7c2 more on "Attributes";
wenzelm
parents: 39839
diff changeset
   160
section {* Morphisms and declarations \label{sec:morphisms} *}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   161
52422
wenzelm
parents: 48985
diff changeset
   162
text {*
wenzelm
parents: 48985
diff changeset
   163
  %FIXME
39877
1206e88f1284 more refs;
wenzelm
parents: 39864
diff changeset
   164
52422
wenzelm
parents: 48985
diff changeset
   165
  See also \cite{Chaieb-Wenzel:2007}.
39877
1206e88f1284 more refs;
wenzelm
parents: 39864
diff changeset
   166
*}
30272
2d612824e642 regenerated document;
wenzelm
parents: 30270
diff changeset
   167
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   168
end