matita/matita/help/C/sec_commands.xml

   1
   2 <!-- ============ Commands ====================== -->
   3 <chapter id="sec_commands">
   4  <title>Other commands</title>
   5  <sect1 id="command_alias">
   6    <title>alias</title>
   7    <para><userinput>alias id &quot;s&quot; = &quot;def&quot;</userinput></para>
   8    <para><userinput>alias symbol &quot;s&quot; (instance n) = &quot;def&quot;</userinput></para>
   9    <para><userinput>alias num (instance n) = &quot;def&quot;</userinput></para>
  10    <para>
  11      <variablelist>
  12        <varlistentry>
  13          <term>Synopsis:</term>
  14          <listitem>
  15            <para><emphasis role="bold">alias</emphasis>
  16             [<emphasis role="bold">id</emphasis> &qstring; <emphasis role="bold">=</emphasis> &qstring;
  17             | <emphasis role="bold">symbol</emphasis> &qstring; [<emphasis role="bold">(instance</emphasis> &nat;<emphasis role="bold">)</emphasis>] <emphasis role="bold">=</emphasis> &qstring;
  18             | <emphasis role="bold">num</emphasis> [<emphasis role="bold">(instance</emphasis> &nat;<emphasis role="bold">)</emphasis>] <emphasis role="bold">=</emphasis> &qstring;
  19             ]
  20            </para>
  21          </listitem>
  22        </varlistentry>
  23        <varlistentry>
  24          <term>Action:</term>
  25          <listitem>
  26            <para>Used to give an hint to the disambiguating parser.
  27             When the parser is faced to the identifier (or symbol)
  28             <command>s</command> or to any number, it will prefer
  29             interpretations that &quot;map <command>s</command> (or the
  30             number) to <command>def</command>&quot;. For identifiers,
  31             &quot;def&quot; is the URI of the interpretation.
  32             E.g.: <command>cic:/matita/nat/nat.ind#xpointer(1/1/1)</command>
  33             for the first constructor of the first inductive type defined
  34             in the block of inductive type(s)
  35             <command>cic:/matita/nat/nat.ind</command>.
  36             For symbols and numbers, &quot;def&quot; is the label used to
  37             mark the wanted
  38             <link linkend="interpretation">interpretation</link>.
  39            </para>
  40           <para>When a symbol or a number occurs several times in the
  41            term to be parsed, it is possible to give an hint only for the
  42            instance <command>n</command>. When the instance is omitted,
  43            the hint is valid for every occurrence.
  44           </para>
  45           <para>
  46            Hints are automatically inserted in the script by Matita every
  47            time the user is interactively asked a question to disambiguate
  48            a term. This way the user won't be posed the same question twice
  49            when the script will be executed again.</para>
  50          </listitem>
  51        </varlistentry>
  52      </variablelist>
  53    </para>
  54  </sect1>
  55  <sect1 id="command_check">
  56    <title>check</title>
  57    <para><userinput>check t</userinput></para>
  58    <para>
  59      <variablelist>
  60        <varlistentry>
  61          <term>Synopsis:</term>
  62          <listitem>
  63            <para><emphasis role="bold">check</emphasis> &sterm;</para>
  64          </listitem>
  65        </varlistentry>
  66        <varlistentry>
  67          <term>Action:</term>
  68          <listitem>
  69            <para>Opens a CIC browser window that shows <command>t</command>
  70             together with its type. The command is immediately removed from
  71             the script.</para>
  72          </listitem>
  73        </varlistentry>
  74      </variablelist>
  75    </para>
  76  </sect1>
  77  <!--
  78  <sect1 id="command_eval">
  79    <title>eval</title>
  80    <para><userinput>eval red on t</userinput></para>
  81    <para>
  82      <variablelist>
  83        <varlistentry>
  84          <term>Synopsis:</term>
  85          <listitem>
  86            <para><emphasis role="bold">eval</emphasis>
  87             &reduction-kind;
  88              <emphasis role="bold">on</emphasis>
  89              &term;</para>
  90          </listitem>
  91        </varlistentry>
  92        <varlistentry>
  93          <term>Action:</term>
  94          <listitem>
  95            <para>Opens a CIC browser window that shows
  96              the reduct of
  97              <command>t</command>
  98              together with its type.</para>
  99          </listitem>
 100        </varlistentry>
 101      </variablelist>
 102    </para>
 103  </sect1>
 104  -->
 105  <!--
 106  <sect1 id="command_prefer_coercion">
 107    <title>prefer coercion</title>
 108    <para><userinput>prefer coercion u</userinput></para>
 109    <para>
 110      <variablelist>
 111        <varlistentry>
 112          <term>Synopsis:</term>
 113          <listitem>
 114                  <para>
 115                          <emphasis role="bold">prefer coercion</emphasis>
 116        (&uri; | &term;)
 117                  </para>
 118          </listitem>
 119        </varlistentry>
 120        <varlistentry>
 121          <term>Action:</term>
 122          <listitem>
 123            <para>The already declared coercion <command>u</command>
 124              is preferred to other coercions with the same source and target.
 125            </para>
 126          </listitem>
 127        </varlistentry>
 128      </variablelist>
 129    </para>
 130  </sect1>
 131  -->
 132  <sect1 id="command_coercion">
 133    <title>coercion</title>
 134    <para>TODO</para>
 135    <!--
 136    <para><userinput>coercion u with ariety saturation nocomposites</userinput></para>
 137    <para>
 138      <variablelist>
 139        <varlistentry>
 140          <term>Synopsis:</term>
 141          <listitem>
 142                  <para>
 143                          <emphasis role="bold">coercion</emphasis>
 144                          (&uri; | &term; <emphasis role="bold">with</emphasis>)
 145                          [ &nat; [&nat;]]
 146                          [ <emphasis role="bold">nocomposites</emphasis> ]
 147                  </para>
 148          </listitem>
 149        </varlistentry>
 150        <varlistentry>
 151          <term>Action:</term>
 152          <listitem>
 153                  <para>Declares <command>u</command> as an implicit coercion.
 154                  If the type of <command>u</command> is
 155                  <command>∀x1:T1. … ∀x(n-1):T(n-1).Tn</command> the coercion target is
 156                  <command>T(n - ariety)</command> while its source is
 157                  <command>T(n - ariety - saturation - 1)</command>.
 158             Every time a term <command>x</command>
 159             of type source is used with expected type target, Matita
 160             automatically replaces <command>x</command> with
 161             <command>(u ? … ? x ? … ?)</command> to avoid a typing error.</para>
 162             Note that the number of <command>?</command> added after
 163             <command>x</command> is saturation.
 164            <para>Implicit coercions are not displayed to the user:
 165             <command>(u ? … ? x)</command> is rendered simply
 166             as <command>x</command>.</para>
 167            <para>When a coercion <command>u</command> is declared
 168             from source <command>s</command> to target <command>t</command>
 169             and there is already a coercion <command>u'</command> of
 170             target <command>s</command> or source <command>t</command>,
 171             a composite implicit coercion is automatically computed
 172             by Matita unless <emphasis role="bold">nocomposites</emphasis>
 173             is specified.</para>
 174          </listitem>
 175        </varlistentry>
 176      </variablelist>
 177    </para>
 178    -->
 179  </sect1>
 180  <!--
 181  <sect1 id="command_default">
 182    <title>default</title>
 183    <para><userinput>default &quot;s&quot; u<subscript>1</subscript> … u<subscript>n</subscript></userinput></para>
 184    <para>
 185      <variablelist>
 186        <varlistentry>
 187          <term>Synopsis:</term>
 188          <listitem>
 189            <para><emphasis role="bold">default</emphasis>
 190             &qstring; &uri; [&uri;]…
 191            </para>
 192          </listitem>
 193        </varlistentry>
 194        <varlistentry>
 195          <term>Action:</term>
 196          <listitem>
 197            <para>It registers a cluster of related definitions and
 198             theorems to be used by tactics and the rendering engine.
 199             Some functionalities of Matita are not available when some
 200             clusters have not been registered. Overloading a cluster
 201             registration is possible: the last registration will be the
 202             default one, but the previous ones are still in effect.</para>
 203            <para>
 204             <command>s</command> is an identifier of the cluster and
 205             <command>u<subscript>1</subscript> … u<subscript>n</subscript></command>
 206             are the URIs of the definitions and theorems of the cluster.
 207             The number <command>n</command> of required URIs depends on the
 208             cluster. The following clusters are supported.
 209            </para>
 210            <table>
 211             <title>clusters</title>
 212             <tgroup cols="6">
 213             <thead>
 214              <row>
 215               <entry>name</entry>
 216               <entry>expected object for 1st URI</entry>
 217               <entry>expected object for 2nd URI</entry>
 218               <entry>expected object for 3rd URI</entry>
 219               <entry>expected object for 4th URI</entry>
 220               <entry>expected object for 5th URI</entry>
 221               <entry>expected object for 6th URI</entry>
 222               <entry>expected object for 7th URI</entry>
 223               <entry>expected object for 8th URI</entry>
 224               <entry>expected object for 9th URI</entry>
 225               <entry>expected object for 10th URI</entry>
 226               <entry>expected object for 11th URI</entry>
 227              </row>
 228             </thead>
 229             <tbody>
 230              <row>
 231               <entry>equality</entry>
 232               <entry>an inductive type (say, of type <command>eq</command>) of type ∀A:Type.A <emphasis role="bold">→</emphasis> <emphasis role="bold">Prop</emphasis> with one family parameter and one constructor of type ∀x:A.eq A x</entry>
 233               <entry>a theorem of type <emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>x,y:A.eq A x y <emphasis role="bold">→</emphasis> eq A y x</entry>
 234               <entry>a theorem of type <emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>x,y,z:A.eq A x y <emphasis role="bold">→</emphasis> eq A y z <emphasis role="bold">→</emphasis> eq A x z</entry>
 235               <entry><emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>a.<emphasis role="bold">∀</emphasis> P:A <emphasis role="bold">→</emphasis> <emphasis role="bold">Prop</emphasis>.P x <emphasis role="bold">→</emphasis> <emphasis role="bold">∀</emphasis>y.eq A x y <emphasis role="bold">→</emphasis> P y</entry>
 236               <entry><emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>a.<emphasis role="bold">∀</emphasis> P:A <emphasis role="bold">→</emphasis> <emphasis role="bold">Prop</emphasis>.P x <emphasis role="bold">→</emphasis> <emphasis role="bold">∀</emphasis>y.eq A y x <emphasis role="bold">→</emphasis> P y</entry>
 237               <entry><emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>a.<emphasis role="bold">∀</emphasis> P:A <emphasis role="bold">→</emphasis> <emphasis role="bold">Set</emphasis>.P x <emphasis role="bold">→</emphasis> <emphasis role="bold">∀</emphasis>y.eq A x y <emphasis role="bold">→</emphasis> P y</entry>
 238               <entry><emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>a.<emphasis role="bold">∀</emphasis> P:A <emphasis role="bold">→</emphasis> <emphasis role="bold">Set</emphasis>.P x <emphasis role="bold">→</emphasis> <emphasis role="bold">∀</emphasis>y.eq A y x <emphasis role="bold">→</emphasis> P y</entry>
 239               <entry><emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>a.<emphasis role="bold">∀</emphasis> P:A <emphasis role="bold">→</emphasis> <emphasis role="bold">Type</emphasis>.P x <emphasis role="bold">→</emphasis> <emphasis role="bold">∀</emphasis>y.eq A x y <emphasis role="bold">→</emphasis> P y</entry>
 240               <entry><emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>a.<emphasis role="bold">∀</emphasis> P:A <emphasis role="bold">→</emphasis> <emphasis role="bold">Type</emphasis>.P x <emphasis role="bold">→</emphasis> <emphasis role="bold">∀</emphasis>y.eq A y x <emphasis role="bold">→</emphasis> P y</entry>
 241               <entry><emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>B.<emphasis role="bold">∀</emphasis> f:A <emphasis role="bold">→</emphasis> B.<emphasis role="bold">∀</emphasis>x,y:A.eq A x y <emphasis role="bold">→</emphasis> eq B (f x) (f y)</entry>
 242               <entry><emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>B.<emphasis role="bold">∀</emphasis> f:A <emphasis role="bold">→</emphasis> B.<emphasis role="bold">∀</emphasis>x,y:A.eq A x y <emphasis role="bold">→</emphasis> eq B (f y) (f x)</entry>
 243              </row>
 244              <row>
 245               <entry>true</entry>
 246               <entry>an inductive type of type <emphasis role="bold">Prop</emphasis> with only one constructor that has no arguments</entry>
 247               <entry/>
 248               <entry/>
 249               <entry/>
 250               <entry/>
 251              </row>
 252              <row>
 253               <entry>false</entry>
 254               <entry>an inductive type of type <emphasis role="bold">Prop</emphasis> without constructors</entry>
 255               <entry/>
 256               <entry/>
 257               <entry/>
 258               <entry/>
 259              </row>
 260              <row>
 261               <entry>absurd</entry>
 262               <entry>a theorem of type <emphasis role="bold">∀</emphasis>A:Prop.<emphasis role="bold">∀</emphasis>B:Prop.A <emphasis role="bold">→</emphasis> Not A <emphasis role="bold">→</emphasis> B</entry>
 263               <entry/>
 264               <entry/>
 265               <entry/>
 266               <entry/>
 267              </row>
 268             </tbody>
 269             </tgroup>
 270            </table>
 271          </listitem>
 272        </varlistentry>
 273      </variablelist>
 274    </para>
 275  </sect1>
 276  -->
 277  <!--
 278  <sect1 id="command_hint">
 279    <title>hint</title>
 280    <para><userinput>hint</userinput></para>
 281    <para>
 282      <variablelist>
 283        <varlistentry>
 284          <term>Synopsis:</term>
 285          <listitem>
 286            <para><emphasis role="bold">hint</emphasis>
 287            </para>
 288          </listitem>
 289        </varlistentry>
 290        <varlistentry>
 291          <term>Action:</term>
 292          <listitem>
 293            <para>Displays a list of theorems that can be successfully
 294             applied to the current selected sequent. The command is
 295             removed from the script, but the window that displays the
 296             theorems allow to add to the script the application of the
 297             selected theorem.
 298            </para>
 299          </listitem>
 300        </varlistentry>
 301      </variablelist>
 302    </para>
 303  </sect1>
 304  -->
 305  <sect1 id="command_include">
 306    <title>include</title>
 307    <para><userinput>include &quot;s&quot;</userinput></para>
 308    <para>
 309      <variablelist>
 310        <varlistentry>
 311          <term>Synopsis:</term>
 312          <listitem>
 313            <para><emphasis role="bold">include</emphasis> &qstring;</para>
 314          </listitem>
 315        </varlistentry>
 316        <varlistentry>
 317          <term>Action:</term>
 318          <listitem>
 319            <para>Every <link linkend="command_coercion">coercion</link>,
 320             <link linkend="notation">notation</link> and
 321             <link linkend="interpretation">interpretation</link> that was active
 322             when the file <command>s</command> was compiled last time
 323             is made active. The same happens for declarations of
 324             <link linkend="command_default">default definitions and
 325             theorems</link> and disambiguation
 326             hints (<link linkend="command_alias">aliases</link>).
 327             On the contrary, theorem and definitions declared in a file can be
 328            immediately used without including it.</para>
 329           <para>The file <command>s</command> is automatically compiled
 330           if it is not compiled yet.
 331           </para>
 332          </listitem>
 333        </varlistentry>
 334      </variablelist>
 335    </para>
 336  </sect1>
 337  <!--
 338  <sect1 id="command_include_first">
 339    <title>include' &quot;s&quot;</title>
 340    <para><userinput></userinput></para>
 341    <para>
 342      <variablelist>
 343        <varlistentry>
 344          <term>Synopsis:</term>
 345          <listitem>
 346            <para><emphasis role="bold">include'</emphasis> &qstring;</para>
 347          </listitem>
 348        </varlistentry>
 349        <varlistentry>
 350          <term>Action:</term>
 351          <listitem>
 352            <para>Not documented (&TODO;), do not use it.</para>
 353          </listitem>
 354        </varlistentry>
 355      </variablelist>
 356    </para>
 357  </sect1>
 358  -->
 359  <!--
 360  <sect1 id="command_whelp">
 361    <title>whelp</title>
 362    <para><userinput>whelp locate &quot;s&quot;</userinput></para>
 363    <para><userinput>whelp hint t</userinput></para>
 364    <para><userinput>whelp elim t</userinput></para>
 365    <para><userinput>whelp match t</userinput></para>
 366    <para><userinput>whelp instance t</userinput></para>
 367    <para>
 368      <variablelist>
 369        <varlistentry>
 370          <term>Synopsis:</term>
 371          <listitem>
 372            <para><emphasis role="bold">whelp</emphasis>
 373             [<emphasis role="bold">locate</emphasis> &qstring;
 374             | <emphasis role="bold">hint</emphasis> &term;
 375             | <emphasis role="bold">elim</emphasis> &term;
 376             | <emphasis role="bold">match</emphasis> &term;
 377             | <emphasis role="bold">instance</emphasis> &term;
 378             ]
 379            </para>
 380          </listitem>
 381        </varlistentry>
 382        <varlistentry>
 383          <term>Action:</term>
 384          <listitem>
 385            <para>Performs the corresponding <link linkend="whelp">query</link>,
 386             showing the result in the CIC browser. The command is removed
 387             from the script.
 388            </para>
 389          </listitem>
 390        </varlistentry>
 391      </variablelist>
 392    </para>
 393  </sect1>
 394  -->
 395  <sect1 id="command_qed">
 396    <title>qed</title>
 397    <para><userinput>qed</userinput></para>
 398    <para>
 399      <variablelist>
 400        <varlistentry>
 401          <term>Synopsis:</term>
 402          <listitem>
 403            <para><emphasis role="bold">qed</emphasis>
 404            </para>
 405          </listitem>
 406        </varlistentry>
 407        <varlistentry>
 408          <term>Action:</term>
 409          <listitem>
 410            <para>Saves and indexes the current interactive theorem or
 411             definition.
 412             In order to do this, the set of sequents still to be proved
 413             must be empty.</para>
 414          </listitem>
 415        </varlistentry>
 416      </variablelist>
 417    </para>
 418  </sect1>
 419  <sect1 id="command_qed_minus">
 420    <title>qed-</title>
 421    <para><userinput>qed-</userinput></para>
 422    <para>
 423      <variablelist>
 424        <varlistentry>
 425          <term>Synopsis:</term>
 426          <listitem>
 427            <para><emphasis role="bold">qed-</emphasis>
 428            </para>
 429          </listitem>
 430        </varlistentry>
 431        <varlistentry>
 432          <term>Action:</term>
 433          <listitem>
 434            <para>Saves the current interactive theorem or
 435             definition without indexing. Therefore automation will ignore
 436             it.
 437             In order to do this, the set of sequents still to be proved
 438             must be empty.</para>
 439          </listitem>
 440        </varlistentry>
 441      </variablelist>
 442    </para>
 443  </sect1>
 444
 445  <!--
 446  <sect1 id="command_inline">
 447    <title>inline</title>
 448    <para><userinput>inline &quot;s&quot; params</userinput></para>
 449    <para>
 450      <variablelist>
 451        <varlistentry>
 452          <term>Synopsis:</term>
 453          <listitem>
 454            <para>
 455              <emphasis role="bold">inline</emphasis> &qstring; &inlineparams;
 456            </para>
 457          </listitem>
 458        </varlistentry>
 459        <varlistentry>
 460          <term>Action:</term>
 461          <listitem>
 462            <para>Inlines a representation of the item <command>s</command>,
 463 which can be the URI of a HELM object. If an entire HELM directory (i.e. a base
 464 URI) or the path of a *.ma source file is provided, all the contained objects
 465 are represented in a row.
 466 If the inlined object has a proof, this proof is represented in several ways
 467 depending on the provided parameters.</para>
 468          </listitem>
 469        </varlistentry>
 470      </variablelist>
 471    </para>
 472
 473     <sect2 id="inline-params">
 474     <title>inline-params</title>
 475     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 476       <title>inline-params</title>
 477       <tgroup cols="4">
 478       <tbody>
 479        <row>
 480         <entry id="grammar.inlineparams">&inlineparams;</entry>
 481         <entry>::=</entry>
 482         <entry>[&inlineparam; [&inlineparam;] … ]</entry>
 483        </row>
 484       </tbody>
 485      </tgroup>
 486     </table>
 487     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 488       <title>inline-param</title>
 489       <tgroup cols="4">
 490       <tbody>
 491
 492        <row>
 493         <entry id="grammar.inlineparam">&inlineparam;</entry>
 494         <entry>::=</entry>
 495         <entry><emphasis role="bold">axiom</emphasis></entry>
 496         <entry>Try to give an <link linkend="axiom">axiom</link> flavour
 497            (bodies are omitted even if present)
 498         </entry>
 499        </row>
 500
 501        <row>
 502         <entry/>
 503         <entry>|</entry>
 504         <entry><emphasis role="bold">definition</emphasis></entry>
 505         <entry>Try give a <link linkend="definition">definition</link> flavour
 506         </entry>
 507        </row>
 508
 509        <row>
 510         <entry/>
 511         <entry>|</entry>
 512         <entry><emphasis role="bold">theorem</emphasis></entry>
 513         <entry>Try give a <link linkend="theorem">theorem</link> flavour
 514         </entry>
 515        </row>
 516
 517        <row>
 518         <entry/>
 519         <entry>|</entry>
 520         <entry><emphasis role="bold">lemma</emphasis></entry>
 521         <entry>Try give a <link linkend="lemma">lemma</link> flavour
 522         </entry>
 523        </row>
 524
 525        <row>
 526         <entry/>
 527         <entry>|</entry>
 528         <entry><emphasis role="bold">remark</emphasis></entry>
 529         <entry>Try give a <link linkend="remark">remark</link> flavour
 530         </entry>
 531        </row>
 532
 533        <row>
 534         <entry/>
 535         <entry>|</entry>
 536         <entry><emphasis role="bold">fact</emphasis></entry>
 537         <entry>Try give a <link linkend="fact">fact</link> flavour
 538         </entry>
 539        </row>
 540
 541        <row>
 542         <entry/>
 543         <entry>|</entry>
 544         <entry><emphasis role="bold">variant</emphasis></entry>
 545         <entry>Try give a <link linkend="variant">variant</link> flavour
 546                (implies <emphasis role="bold">plain</emphasis>)
 547         </entry>
 548        </row>
 549
 550        <row>
 551         <entry/>
 552         <entry>|</entry>
 553         <entry><emphasis role="bold">declarative</emphasis></entry>
 554         <entry>Represent proofs using
 555            <link linkend="sec_declarative_tactics">declarative tactics</link>
 556            (this is the dafault and can be omitted)
 557         </entry>
 558        </row>
 559
 560        <row>
 561         <entry/>
 562         <entry>|</entry>
 563         <entry><emphasis role="bold">procedural</emphasis></entry>
 564         <entry>Represent proofs using
 565            <link linkend="sec_tactics">procedural tactics</link>
 566         </entry>
 567        </row>
 568
 569        <row>
 570         <entry/>
 571         <entry>|</entry>
 572         <entry><emphasis role="bold">plain</emphasis></entry>
 573         <entry>Represent proofs using plain
 574            <link linkend="tbl_terms">proof terms</link>
 575         </entry>
 576        </row>
 577
 578        <row>
 579         <entry/>
 580         <entry>|</entry>
 581         <entry><emphasis role="bold">nodefaults</emphasis></entry>
 582         <entry>
 583          Do not use the tactics depending on the
 584          <link linkend="command_default">default</link> command
 585            (<link linkend="tac_rewrite">rewrite</link>
 586             in the <emphasis role="bold">procedural</emphasis> mode)
 587         </entry>
 588        </row>
 589
 590        <row valign="top">
 591         <entry/>
 592         <entry>|</entry>
 593         <entry><emphasis role="bold">level=&nat;</emphasis></entry>
 594         <entry>
 595          Set the level of the procedural proof representation
 596          (the default is the highest level)
 597          <itemizedlist>
 598           <listitem>
 599            Tactics used at level 1:
 600             <link linkend="tac_exact">exact</link>
 601           </listitem>
 602           <listitem>
 603            Additional tactics used at level 2:
 604             <link linkend="tac_letin">letin</link>,
 605             <link linkend="tac_cut">cut</link>,
 606             <link linkend="tac_change">change</link>,
 607             <link linkend="tac_intros">intros</link>,
 608             <link linkend="tac_apply">apply</link>,
 609             <link linkend="tac_elim">elim</link>,
 610             <link linkend="tac_cases">cases</link>,
 611             <link linkend="tac_rewrite">rewrite</link>
 612           </listitem>
 613          </itemizedlist>
 614         </entry>
 615        </row>
 616
 617        <row>
 618         <entry/>
 619         <entry>|</entry>
 620         <entry><emphasis role="bold">depth=&nat;</emphasis></entry>
 621         <entry>&TODO;</entry>
 622        </row>
 623
 624       </tbody>
 625      </tgroup>
 626     </table>
 627     </sect2>
 628  </sect1>
 629  -->
 630 </chapter>