src/Doc/Isar_Ref/Proof_Script.thy
author wenzelm
Mon, 15 Jun 2015 14:10:41 +0200
changeset 60484 98ee86354354
child 60631 441fdbfbb2d3
permissions -rw-r--r--
moved sections;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
60484
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
     1
theory Proof_Script
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
     2
imports Base Main
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
     3
begin
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
     4
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
     5
chapter \<open>Proof scripts\<close>
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
     6
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
     7
text \<open>
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
     8
  Interactive theorem proving is traditionally associated with ``proof
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
     9
  scripts'', but Isabelle/Isar is centered around structured \emph{proof
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    10
  documents} instead (see also \chref{ch:proofs}).
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    11
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    12
  Nonetheless, it is possible to emulate proof scripts by sequential
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    13
  refinements of a proof state in backwards mode, notably with the @{command
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    14
  apply} command (see \secref{sec:tactic-commands}). There are also various
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    15
  proof methods that allow to refer to implicit goal state information that
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    16
  is normally not accessible to structured Isar proofs (see
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    17
  \secref{sec:tactics}).
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    18
\<close>
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    19
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    20
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    21
section \<open>Commands for step-wise refinement \label{sec:tactic-commands}\<close>
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    22
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    23
text \<open>
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    24
  \begin{matharray}{rcl}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    25
    @{command_def "supply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    26
    @{command_def "apply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    27
    @{command_def "apply_end"}@{text "\<^sup>*"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    28
    @{command_def "done"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    29
    @{command_def "defer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    30
    @{command_def "prefer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    31
    @{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    32
  \end{matharray}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    33
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    34
  @{rail \<open>
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    35
    @@{command supply} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    36
    ;
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    37
    ( @@{command apply} | @@{command apply_end} ) @{syntax method}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    38
    ;
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    39
    @@{command defer} @{syntax nat}?
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    40
    ;
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    41
    @@{command prefer} @{syntax nat}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    42
  \<close>}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    43
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    44
  \begin{description}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    45
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    46
  \item @{command "supply"} supports fact definitions during goal
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    47
  refinement: it is similar to @{command "note"}, but it operates in
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    48
  backwards mode and does not have any impact on chained facts.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    49
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    50
  \item @{command "apply"}~@{text m} applies proof method @{text m} in
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    51
  initial position, but unlike @{command "proof"} it retains ``@{text
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    52
  "proof(prove)"}'' mode.  Thus consecutive method applications may be
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    53
  given just as in tactic scripts.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    54
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    55
  Facts are passed to @{text m} as indicated by the goal's
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    56
  forward-chain mode, and are \emph{consumed} afterwards.  Thus any
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    57
  further @{command "apply"} command would always work in a purely
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    58
  backward manner.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    59
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    60
  \item @{command "apply_end"}~@{text "m"} applies proof method @{text
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    61
  m} as if in terminal position.  Basically, this simulates a
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    62
  multi-step tactic script for @{command "qed"}, but may be given
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    63
  anywhere within the proof body.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    64
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    65
  No facts are passed to @{text m} here.  Furthermore, the static
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    66
  context is that of the enclosing goal (as for actual @{command
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    67
  "qed"}).  Thus the proof method may not refer to any assumptions
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    68
  introduced in the current body, for example.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    69
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    70
  \item @{command "done"} completes a proof script, provided that the
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    71
  current goal state is solved completely.  Note that actual
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    72
  structured proof commands (e.g.\ ``@{command "."}'' or @{command
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    73
  "sorry"}) may be used to conclude proof scripts as well.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    74
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    75
  \item @{command "defer"}~@{text n} and @{command "prefer"}~@{text n}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    76
  shuffle the list of pending goals: @{command "defer"} puts off
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    77
  sub-goal @{text n} to the end of the list (@{text "n = 1"} by
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    78
  default), while @{command "prefer"} brings sub-goal @{text n} to the
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    79
  front.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    80
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    81
  \item @{command "back"} does back-tracking over the result sequence
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    82
  of the latest proof command.  Any proof command may return multiple
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    83
  results, and this command explores the possibilities step-by-step.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    84
  It is mainly useful for experimentation and interactive exploration,
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    85
  and should be avoided in finished proofs.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    86
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    87
  \end{description}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    88
\<close>
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    89
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    90
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    91
section \<open>Tactics: improper proof methods \label{sec:tactics}\<close>
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    92
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    93
text \<open>
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    94
  The following improper proof methods emulate traditional tactics.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    95
  These admit direct access to the goal state, which is normally
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    96
  considered harmful!  In particular, this may involve both numbered
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    97
  goal addressing (default 1), and dynamic instantiation within the
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    98
  scope of some subgoal.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    99
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   100
  \begin{warn}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   101
    Dynamic instantiations refer to universally quantified parameters
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   102
    of a subgoal (the dynamic context) rather than fixed variables and
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   103
    term abbreviations of a (static) Isar context.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   104
  \end{warn}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   105
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   106
  Tactic emulation methods, unlike their ML counterparts, admit
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   107
  simultaneous instantiation from both dynamic and static contexts.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   108
  If names occur in both contexts goal parameters hide locally fixed
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   109
  variables.  Likewise, schematic variables refer to term
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   110
  abbreviations, if present in the static context.  Otherwise the
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   111
  schematic variable is interpreted as a schematic variable and left
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   112
  to be solved by unification with certain parts of the subgoal.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   113
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   114
  Note that the tactic emulation proof methods in Isabelle/Isar are
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   115
  consistently named @{text foo_tac}.  Note also that variable names
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   116
  occurring on left hand sides of instantiations must be preceded by a
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   117
  question mark if they coincide with a keyword or contain dots.  This
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   118
  is consistent with the attribute @{attribute "where"} (see
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   119
  \secref{sec:pure-meth-att}).
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   120
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   121
  \begin{matharray}{rcl}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   122
    @{method_def rule_tac}@{text "\<^sup>*"} & : & @{text method} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   123
    @{method_def erule_tac}@{text "\<^sup>*"} & : & @{text method} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   124
    @{method_def drule_tac}@{text "\<^sup>*"} & : & @{text method} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   125
    @{method_def frule_tac}@{text "\<^sup>*"} & : & @{text method} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   126
    @{method_def cut_tac}@{text "\<^sup>*"} & : & @{text method} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   127
    @{method_def thin_tac}@{text "\<^sup>*"} & : & @{text method} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   128
    @{method_def subgoal_tac}@{text "\<^sup>*"} & : & @{text method} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   129
    @{method_def rename_tac}@{text "\<^sup>*"} & : & @{text method} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   130
    @{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   131
    @{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   132
    @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   133
  \end{matharray}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   134
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   135
  @{rail \<open>
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   136
    (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   137
      @@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \<newline>
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   138
    (@{syntax named_insts} @{syntax for_fixes} @'in' @{syntax thmref} | @{syntax thmrefs} )
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   139
    ;
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   140
    @@{method thin_tac} @{syntax goal_spec}? @{syntax prop} @{syntax for_fixes}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   141
    ;
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   142
    @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) @{syntax for_fixes}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   143
    ;
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   144
    @@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   145
    ;
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   146
    @@{method rotate_tac} @{syntax goal_spec}? @{syntax int}?
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   147
    ;
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   148
    (@@{method tactic} | @@{method raw_tactic}) @{syntax text}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   149
  \<close>}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   150
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   151
\begin{description}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   152
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   153
  \item @{method rule_tac} etc. do resolution of rules with explicit
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   154
  instantiation.  This works the same way as the ML tactics @{ML
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   155
  Rule_Insts.res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}).
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   156
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   157
  Multiple rules may be only given if there is no instantiation; then
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   158
  @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   159
  @{cite "isabelle-implementation"}).
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   160
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   161
  \item @{method cut_tac} inserts facts into the proof state as
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   162
  assumption of a subgoal; instantiations may be given as well.  Note
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   163
  that the scope of schematic variables is spread over the main goal
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   164
  statement and rule premises are turned into new subgoals.  This is
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   165
  in contrast to the regular method @{method insert} which inserts
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   166
  closed rule statements.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   167
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   168
  \item @{method thin_tac}~@{text \<phi>} deletes the specified premise
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   169
  from a subgoal.  Note that @{text \<phi>} may contain schematic
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   170
  variables, to abbreviate the intended proposition; the first
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   171
  matching subgoal premise will be deleted.  Removing useless premises
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   172
  from a subgoal increases its readability and can make search tactics
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   173
  run faster.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   174
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   175
  \item @{method subgoal_tac}~@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} adds the propositions
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   176
  @{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} as local premises to a subgoal, and poses the same
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   177
  as new subgoals (in the original context).
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   178
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   179
  \item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   180
  goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   181
  \emph{suffix} of variables.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   182
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   183
  \item @{method rotate_tac}~@{text n} rotates the premises of a
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   184
  subgoal by @{text n} positions: from right to left if @{text n} is
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   185
  positive, and from left to right if @{text n} is negative; the
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   186
  default value is 1.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   187
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   188
  \item @{method tactic}~@{text "text"} produces a proof method from
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   189
  any ML text of type @{ML_type tactic}.  Apart from the usual ML
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   190
  environment and the current proof context, the ML code may refer to
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   191
  the locally bound values @{ML_text facts}, which indicates any
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   192
  current facts used for forward-chaining.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   193
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   194
  \item @{method raw_tactic} is similar to @{method tactic}, but
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   195
  presents the goal state in its raw internal form, where simultaneous
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   196
  subgoals appear as conjunction of the logical framework instead of
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   197
  the usual split into several subgoals.  While feature this is useful
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   198
  for debugging of complex method definitions, it should not never
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   199
  appear in production theories.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   200
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   201
  \end{description}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   202
\<close>
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   203
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   204
end