<varlistentry>
<term>Synopsis:</term>
<listitem>
- <para><emphasis role="bold">check</emphasis> &term;</para>
+ <para><emphasis role="bold">check</emphasis> &sterm;</para>
</listitem>
</varlistentry>
<varlistentry>
</variablelist>
</para>
</sect1>
+ <!--
<sect1 id="command_eval">
<title>eval</title>
<para><userinput>eval red on t</userinput></para>
</variablelist>
</para>
</sect1>
+ -->
+ <!--
<sect1 id="command_prefer_coercion">
<title>prefer coercion</title>
<para><userinput>prefer coercion u</userinput></para>
</variablelist>
</para>
</sect1>
+ -->
<sect1 id="command_coercion">
<title>coercion</title>
+ <para>TODO</para>
+ <!--
<para><userinput>coercion u with ariety saturation nocomposites</userinput></para>
<para>
<variablelist>
</varlistentry>
</variablelist>
</para>
+ -->
</sect1>
+ <!--
<sect1 id="command_default">
<title>default</title>
<para><userinput>default "s" u<subscript>1</subscript> … u<subscript>n</subscript></userinput></para>
</variablelist>
</para>
</sect1>
+ -->
+ <!--
<sect1 id="command_hint">
<title>hint</title>
<para><userinput>hint</userinput></para>
</variablelist>
</para>
</sect1>
+ -->
<sect1 id="command_include">
<title>include</title>
<para><userinput>include "s"</userinput></para>
</variablelist>
</para>
</sect1>
+ <!--
<sect1 id="command_include_first">
<title>include' "s"</title>
<para><userinput></userinput></para>
</variablelist>
</para>
</sect1>
+ -->
+ <!--
<sect1 id="command_whelp">
<title>whelp</title>
<para><userinput>whelp locate "s"</userinput></para>
</variablelist>
</para>
</sect1>
+ -->
<sect1 id="command_qed">
<title>qed</title>
<para><userinput>qed</userinput></para>
</variablelist>
</para>
</sect1>
+ <sect1 id="command_qed_minus">
+ <title>qed-</title>
+ <para><userinput>qed-</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">qed-</emphasis>
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>Saves the current interactive theorem or
+ definition without indexing. Therefore automation will ignore
+ it.
+ In order to do this, the set of sequents still to be proved
+ must be empty.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <!--
<sect1 id="command_inline">
<title>inline</title>
<para><userinput>inline "s" params</userinput></para>
</table>
</sect2>
</sect1>
+ -->
</chapter>