+ <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>