<!-- ================= Tactics ========================= -->
<chapter id="sec_declarative_tactics">
- <title> Tactics Declarative</title>
+ <title>Declarative Tactics</title>
<sect1
id="declarative_tactics_quickref">
<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>
<sect1 id="tac_obtain">
- <title>obtain</title>
- <titleabbrev>obtain</titleabbrev>
- <para><userinput>obtain t=t by [t|_]</userinput></para>
+ <title>obtain/conclude</title>
+ <titleabbrev>obtain/conclude</titleabbrev>
+ <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> &term; <emphasis role="bold">=</emphasis> &term; <emphasis role="bold">by</emphasis> [ &term; | _ ]</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>