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           <para>
 333           If the file <command>s</command> was already included, either
 334           directly or recursively, the commands does nothing.
 335           </para>
 336          </listitem>
 337        </varlistentry>
 338      </variablelist>
 339    </para>
 340  </sect1>
 341  <sect1 id="command_include_alias">
 342    <title>include alias</title>
 343    <para><userinput>include alias &quot;s&quot;</userinput></para>
 344    <para>
 345      <variablelist>
 346        <varlistentry>
 347          <term>Synopsis:</term>
 348          <listitem>
 349            <para><emphasis role="bold">include</emphasis> <emphasis role="bold">alias</emphasis> &qstring;</para>
 350          </listitem>
 351        </varlistentry>
 352        <varlistentry>
 353          <term>Action:</term>
 354          <listitem>
 355            <para>Every
 356             <link linkend="interpretation">interpretation</link>
 357             declared in the file <command>s</command> is re-declared
 358             so to make it the preferred choice for disambiguation.
 359           </para>
 360          </listitem>
 361        </varlistentry>
 362      </variablelist>
 363    </para>
 364  </sect1>
 365  <!--
 366  <sect1 id="command_include_first">
 367    <title>include' &quot;s&quot;</title>
 368    <para><userinput></userinput></para>
 369    <para>
 370      <variablelist>
 371        <varlistentry>
 372          <term>Synopsis:</term>
 373          <listitem>
 374            <para><emphasis role="bold">include'</emphasis> &qstring;</para>
 375          </listitem>
 376        </varlistentry>
 377        <varlistentry>
 378          <term>Action:</term>
 379          <listitem>
 380            <para>Not documented (&TODO;), do not use it.</para>
 381          </listitem>
 382        </varlistentry>
 383      </variablelist>
 384    </para>
 385  </sect1>
 386  -->
 387  <!--
 388  <sect1 id="command_whelp">
 389    <title>whelp</title>
 390    <para><userinput>whelp locate &quot;s&quot;</userinput></para>
 391    <para><userinput>whelp hint t</userinput></para>
 392    <para><userinput>whelp elim t</userinput></para>
 393    <para><userinput>whelp match t</userinput></para>
 394    <para><userinput>whelp instance t</userinput></para>
 395    <para>
 396      <variablelist>
 397        <varlistentry>
 398          <term>Synopsis:</term>
 399          <listitem>
 400            <para><emphasis role="bold">whelp</emphasis>
 401             [<emphasis role="bold">locate</emphasis> &qstring;
 402             | <emphasis role="bold">hint</emphasis> &term;
 403             | <emphasis role="bold">elim</emphasis> &term;
 404             | <emphasis role="bold">match</emphasis> &term;
 405             | <emphasis role="bold">instance</emphasis> &term;
 406             ]
 407            </para>
 408          </listitem>
 409        </varlistentry>
 410        <varlistentry>
 411          <term>Action:</term>
 412          <listitem>
 413            <para>Performs the corresponding <link linkend="whelp">query</link>,
 414             showing the result in the CIC browser. The command is removed
 415             from the script.
 416            </para>
 417          </listitem>
 418        </varlistentry>
 419      </variablelist>
 420    </para>
 421  </sect1>
 422  -->
 423  <sect1 id="command_qed">
 424    <title>qed</title>
 425    <para><userinput>qed</userinput></para>
 426    <para>
 427      <variablelist>
 428        <varlistentry>
 429          <term>Synopsis:</term>
 430          <listitem>
 431            <para><emphasis role="bold">qed</emphasis>
 432            </para>
 433          </listitem>
 434        </varlistentry>
 435        <varlistentry>
 436          <term>Action:</term>
 437          <listitem>
 438            <para>Saves and indexes the current interactive theorem or
 439             definition.
 440             In order to do this, the set of sequents still to be proved
 441             must be empty.</para>
 442          </listitem>
 443        </varlistentry>
 444      </variablelist>
 445    </para>
 446  </sect1>
 447  <sect1 id="command_qed_minus">
 448    <title>qed-</title>
 449    <para><userinput>qed-</userinput></para>
 450    <para>
 451      <variablelist>
 452        <varlistentry>
 453          <term>Synopsis:</term>
 454          <listitem>
 455            <para><emphasis role="bold">qed-</emphasis>
 456            </para>
 457          </listitem>
 458        </varlistentry>
 459        <varlistentry>
 460          <term>Action:</term>
 461          <listitem>
 462            <para>Saves the current interactive theorem or
 463             definition without indexing. Therefore automation will ignore
 464             it.
 465             In order to do this, the set of sequents still to be proved
 466             must be empty.</para>
 467          </listitem>
 468        </varlistentry>
 469      </variablelist>
 470    </para>
 471  </sect1>
 472
 473  <!--
 474  <sect1 id="command_inline">
 475    <title>inline</title>
 476    <para><userinput>inline &quot;s&quot; params</userinput></para>
 477    <para>
 478      <variablelist>
 479        <varlistentry>
 480          <term>Synopsis:</term>
 481          <listitem>
 482            <para>
 483              <emphasis role="bold">inline</emphasis> &qstring; &inlineparams;
 484            </para>
 485          </listitem>
 486        </varlistentry>
 487        <varlistentry>
 488          <term>Action:</term>
 489          <listitem>
 490            <para>Inlines a representation of the item <command>s</command>,
 491 which can be the URI of a HELM object. If an entire HELM directory (i.e. a base
 492 URI) or the path of a *.ma source file is provided, all the contained objects
 493 are represented in a row.
 494 If the inlined object has a proof, this proof is represented in several ways
 495 depending on the provided parameters.</para>
 496          </listitem>
 497        </varlistentry>
 498      </variablelist>
 499    </para>
 500
 501     <sect2 id="inline-params">
 502     <title>inline-params</title>
 503     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 504       <title>inline-params</title>
 505       <tgroup cols="4">
 506       <tbody>
 507        <row>
 508         <entry id="grammar.inlineparams">&inlineparams;</entry>
 509         <entry>::=</entry>
 510         <entry>[&inlineparam; [&inlineparam;] … ]</entry>
 511        </row>
 512       </tbody>
 513      </tgroup>
 514     </table>
 515     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 516       <title>inline-param</title>
 517       <tgroup cols="4">
 518       <tbody>
 519
 520        <row>
 521         <entry id="grammar.inlineparam">&inlineparam;</entry>
 522         <entry>::=</entry>
 523         <entry><emphasis role="bold">axiom</emphasis></entry>
 524         <entry>Try to give an <link linkend="axiom">axiom</link> flavour
 525            (bodies are omitted even if present)
 526         </entry>
 527        </row>
 528
 529        <row>
 530         <entry/>
 531         <entry>|</entry>
 532         <entry><emphasis role="bold">definition</emphasis></entry>
 533         <entry>Try give a <link linkend="definition">definition</link> flavour
 534         </entry>
 535        </row>
 536
 537        <row>
 538         <entry/>
 539         <entry>|</entry>
 540         <entry><emphasis role="bold">theorem</emphasis></entry>
 541         <entry>Try give a <link linkend="theorem">theorem</link> flavour
 542         </entry>
 543        </row>
 544
 545        <row>
 546         <entry/>
 547         <entry>|</entry>
 548         <entry><emphasis role="bold">lemma</emphasis></entry>
 549         <entry>Try give a <link linkend="lemma">lemma</link> flavour
 550         </entry>
 551        </row>
 552
 553        <row>
 554         <entry/>
 555         <entry>|</entry>
 556         <entry><emphasis role="bold">remark</emphasis></entry>
 557         <entry>Try give a <link linkend="remark">remark</link> flavour
 558         </entry>
 559        </row>
 560
 561        <row>
 562         <entry/>
 563         <entry>|</entry>
 564         <entry><emphasis role="bold">fact</emphasis></entry>
 565         <entry>Try give a <link linkend="fact">fact</link> flavour
 566         </entry>
 567        </row>
 568
 569        <row>
 570         <entry/>
 571         <entry>|</entry>
 572         <entry><emphasis role="bold">variant</emphasis></entry>
 573         <entry>Try give a <link linkend="variant">variant</link> flavour
 574                (implies <emphasis role="bold">plain</emphasis>)
 575         </entry>
 576        </row>
 577
 578        <row>
 579         <entry/>
 580         <entry>|</entry>
 581         <entry><emphasis role="bold">declarative</emphasis></entry>
 582         <entry>Represent proofs using
 583            <link linkend="sec_declarative_tactics">declarative tactics</link>
 584            (this is the dafault and can be omitted)
 585         </entry>
 586        </row>
 587
 588        <row>
 589         <entry/>
 590         <entry>|</entry>
 591         <entry><emphasis role="bold">procedural</emphasis></entry>
 592         <entry>Represent proofs using
 593            <link linkend="sec_tactics">procedural tactics</link>
 594         </entry>
 595        </row>
 596
 597        <row>
 598         <entry/>
 599         <entry>|</entry>
 600         <entry><emphasis role="bold">plain</emphasis></entry>
 601         <entry>Represent proofs using plain
 602            <link linkend="tbl_terms">proof terms</link>
 603         </entry>
 604        </row>
 605
 606        <row>
 607         <entry/>
 608         <entry>|</entry>
 609         <entry><emphasis role="bold">nodefaults</emphasis></entry>
 610         <entry>
 611          Do not use the tactics depending on the
 612          <link linkend="command_default">default</link> command
 613            (<link linkend="tac_rewrite">rewrite</link>
 614             in the <emphasis role="bold">procedural</emphasis> mode)
 615         </entry>
 616        </row>
 617
 618        <row valign="top">
 619         <entry/>
 620         <entry>|</entry>
 621         <entry><emphasis role="bold">level=&nat;</emphasis></entry>
 622         <entry>
 623          Set the level of the procedural proof representation
 624          (the default is the highest level)
 625          <itemizedlist>
 626           <listitem>
 627            Tactics used at level 1:
 628             <link linkend="tac_exact">exact</link>
 629           </listitem>
 630           <listitem>
 631            Additional tactics used at level 2:
 632             <link linkend="tac_letin">letin</link>,
 633             <link linkend="tac_cut">cut</link>,
 634             <link linkend="tac_change">change</link>,
 635             <link linkend="tac_intros">intros</link>,
 636             <link linkend="tac_apply">apply</link>,
 637             <link linkend="tac_elim">elim</link>,
 638             <link linkend="tac_cases">cases</link>,
 639             <link linkend="tac_rewrite">rewrite</link>
 640           </listitem>
 641          </itemizedlist>
 642         </entry>
 643        </row>
 644
 645        <row>
 646         <entry/>
 647         <entry>|</entry>
 648         <entry><emphasis role="bold">depth=&nat;</emphasis></entry>
 649         <entry>&TODO;</entry>
 650        </row>
 651
 652       </tbody>
 653      </tgroup>
 654     </table>
 655     </sect2>
 656  </sect1>
 657  -->
 658 </chapter>