<varlistentry>
<term>Pre-condition:</term>
<listitem>
- <para> Da Fare </para>
+ <para> &TODO; </para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para> Da Fare </para>
+ <para> &TODO; </para>
</listitem>
</varlistentry>
<varlistentry>
<varlistentry>
<term>Pre-condition:</term>
<listitem>
- <para> Da Fare </para>
+ <para> &TODO; </para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para> Da Fare </para>
+ <para> &TODO; </para>
</listitem>
</varlistentry>
<varlistentry>
<varlistentry>
<term>Pre-condition:</term>
<listitem>
- <para> Da Fare </para>
+ <para> &TODO; </para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para> Da Fare </para>
+ <para> &TODO; </para>
</listitem>
</varlistentry>
<varlistentry>
<varlistentry>
<term>Pre-condition:</term>
<listitem>
- <para> Da Fare </para>
+ <para> &TODO; </para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para> Da Fare </para>
+ <para> &TODO; </para>
</listitem>
</varlistentry>
<varlistentry>
<varlistentry>
<term>Pre-condition:</term>
<listitem>
- <para> Da Fare </para>
+ <para> &TODO; </para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para> Da Fare </para>
+ <para> &TODO; </para>
</listitem>
</varlistentry>
<varlistentry>
<term>New sequents to prove:</term>
<listitem>
- <para>Da Fare</para>
+ <para>&TODO;</para>
</listitem>
</varlistentry>
</variablelist>
<sect1 id="tac_obtain">
<title>obtain/conclude</title>
<titleabbrev>obtain/conclude</titleabbrev>
- <para><userinput>obtain H t=t by [t|_] done</userinput></para>
+ <para><userinput>obtain H t=t [auto_params | exact t| proof | using t] done</userinput></para>
<para>
<variablelist>
<varlistentry role="tactic.synopsis">
<term>Synopsis:</term>
<listitem>
- <para>[<emphasis role="bold">obtain</emphasis> &id; | <emphasis role="bold">conclude</emphasis> &term;] <emphasis role="bold">=</emphasis> &term; <emphasis role="bold">by</emphasis> [ &term; | <emphasis role="bold">_</emphasis> [<emphasis role="bold">(</emphasis>&autoparams;<emphasis role="bold">)</emphasis>]] [<emphasis role="bold">done</emphasis>]</para>
+ <para>[<emphasis role="bold">obtain</emphasis> &id; | <emphasis role="bold">conclude</emphasis> &term;] <emphasis role="bold">=</emphasis> &term; [&autoparams; | <emphasis role="bold">exact</emphasis> &term; | <emphasis role="bold">using</emphasis> &term; | <emphasis role="bold">proof</emphasis>] [<emphasis role="bold">done</emphasis>]</para>
</listitem>
</varlistentry>
<varlistentry>
<term>Pre-condition:</term>
<listitem>
- <para> Da Fare </para>
+ <para> &TODO; </para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para> Da Fare </para>
+ <para> &TODO; </para>
</listitem>
</varlistentry>
<varlistentry>
<term>New sequence to prove:</term>
<listitem>
- <para> Da Fare </para>
+ <para> &TODO; </para>
</listitem>
</varlistentry>
</variablelist>
<varlistentry>
<term>New sequence to prove:</term>
<listitem>
- <para> Da fare </para>
+ <para> &TODO; </para>
</listitem>
</varlistentry>
</variablelist>