+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">definition</emphasis></entry>
+ <entry>Try give a <link linkend="definition">definition</link> flavour
+ </entry>
+ </row>
+
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">theorem</emphasis></entry>
+ <entry>Try give a <link linkend="theorem">theorem</link> flavour
+ </entry>
+ </row>
+
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">lemma</emphasis></entry>
+ <entry>Try give a <link linkend="lemma">lemma</link> flavour
+ </entry>
+ </row>
+
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">remark</emphasis></entry>
+ <entry>Try give a <link linkend="remark">remark</link> flavour
+ </entry>
+ </row>
+
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">fact</emphasis></entry>
+ <entry>Try give a <link linkend="fact">fact</link> flavour
+ </entry>
+ </row>
+
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">variant</emphasis></entry>
+ <entry>Try give a <link linkend="variant">variant</link> flavour
+ (implies <emphasis role="bold">plain</emphasis>)
+ </entry>
+ </row>
+
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">declarative</emphasis></entry>
+ <entry>Represent proofs using
+ <link linkend="sec_declarative_tactics">declarative tactics</link>
+ (this is the dafault and can be omitted)
+ </entry>
+ </row>
+
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">procedural</emphasis></entry>
+ <entry>Represent proofs using
+ <link linkend="sec_tactics">procedural tactics</link>
+ </entry>
+ </row>
+
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">plain</emphasis></entry>
+ <entry>Represent proofs using plain
+ <link linkend="tbl_terms">proof terms</link>
+ </entry>
+ </row>
+
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">nodefaults</emphasis></entry>
+ <entry>
+ Do not use the tactics depending on the
+ <link linkend="command_default">default</link> command
+ (<link linkend="tac_rewrite">rewrite</link>
+ in the <emphasis role="bold">procedural</emphasis> mode)
+ </entry>
+ </row>
+
+ <row valign="top">
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">level=&nat;</emphasis></entry>
+ <entry>
+ Set the level of the procedural proof representation
+ (the default is the highest level)
+ <itemizedlist>
+ <listitem>
+ Tactics used at level 1:
+ <link linkend="tac_exact">exact</link>
+ </listitem>
+ <listitem>
+ Additional tactics used at level 2:
+ <link linkend="tac_letin">letin</link>,
+ <link linkend="tac_cut">cut</link>,
+ <link linkend="tac_change">change</link>,
+ <link linkend="tac_intros">intros</link>,
+ <link linkend="tac_apply">apply</link>,
+ <link linkend="tac_elim">elim</link>,
+ <link linkend="tac_cases">cases</link>,
+ <link linkend="tac_rewrite">rewrite</link>
+ </listitem>
+ </itemizedlist>
+ </entry>
+ </row>
+
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">depth=&nat;</emphasis></entry>
+ <entry>&TODO;</entry>
+ </row>
+
+ </tbody>
+ </tgroup>
+ </table>
+ </sect2>
+ </sect1>
+</chapter>