<!-- ============ Tactics ====================== -->
-<sect1 id="sec_tactics">
+<chapter id="sec_tactics">
<title>Tactics</title>
- <sect2 id="tac_absurd">
+ <sect1 id="tac_absurd">
<title>absurd <term></title>
<para><userinput>absurd P</userinput></para>
- <para>
+ <para>
+ <variablelist>
<varlistentry>
<term>Pre-conditions:</term>
<listitem>
<para><command>P</command> must have type <command>Prop</command>.</para>
</listitem>
</varlistentry>
- <variablelist>
<varlistentry>
<term>Action:</term>
<listitem>
</listitem>
</varlistentry>
</variablelist>
- </para>
- </sect2>
- <sect2 id="tac_apply">
+ </para>
+ </sect1>
+ <sect1 id="tac_apply">
<title>apply <term></title>
<para><userinput>apply t</userinput></para>
<para>
</varlistentry>
</variablelist>
</para>
- </sect2>
- <sect2 id="tac_assumption">
+ </sect1>
+ <sect1 id="tac_assumption">
<title>assumption</title>
- <para><userinput>assumption</userinput></para>
+ <para><userinput>assumption </userinput></para>
<para>
<variablelist>
<varlistentry>
</varlistentry>
</variablelist>
</para>
- </sect2>
- <sect2 id="tac_auto">
+ </sect1>
+ <sect1 id="tac_auto">
<title>auto [depth=<int>] [width=<int>] [paramodulation] [full]</title>
<para><userinput>auto depth=d width=w paramodulation full</userinput></para>
<para>
</varlistentry>
</variablelist>
</para>
- </sect2>
- <sect2 id="tac_clear">
+ </sect1>
+ <sect1 id="tac_clear">
<title>clear <id></title>
<para><userinput>clear H</userinput></para>
<para>
</varlistentry>
</variablelist>
</para>
- </sect2>
- <sect2 id="tac_clearbody">
+ </sect1>
+ <sect1 id="tac_clearbody">
<title>clearbody <id></title>
<para><userinput>clearbody H</userinput></para>
<para>
</varlistentry>
</variablelist>
</para>
- </sect2>
- <sect2 id="tac_change">
+ </sect1>
+ <sect1 id="tac_change">
<title>change <pattern> with <term></title>
<para><userinput>change patt with t</userinput></para>
<para>
</varlistentry>
</variablelist>
</para>
- </sect2>
- <sect2 id="tac_constructor">
+ </sect1>
+ <sect1 id="tac_constructor">
<title>constructor <int></title>
<para><userinput>constructor n</userinput></para>
<para>
</varlistentry>
</variablelist>
</para>
- </sect2>
- <sect2 id="tac_contradiction">
+ </sect1>
+ <sect1 id="tac_contradiction">
<title>contradiction</title>
- <para><userinput>contradiction</userinput></para>
+ <para><userinput>contradiction </userinput></para>
<para>
<variablelist>
<varlistentry>
</varlistentry>
</variablelist>
</para>
- </sect2>
- <sect2 id="tac_cut">
+ </sect1>
+ <sect1 id="tac_cut">
<title>cut <term> [as <id>]</title>
<para><userinput>cut P as H</userinput></para>
<para>
</varlistentry>
</variablelist>
</para>
- </sect2>
- <sect2 id="tac_decompose">
+ </sect1>
+ <sect1 id="tac_decompose">
<title>decompose [<ident list>] <ident> [<intros_spec>]</title>
<para><userinput>decompose ???</userinput></para>
<para>
</varlistentry>
</variablelist>
</para>
- </sect2>
- <sect2 id="tac_discriminate">
+ </sect1>
+ <sect1 id="tac_discriminate">
<title>discriminate <term></title>
<para><userinput>discriminate p</userinput></para>
<para>
</varlistentry>
</variablelist>
</para>
- </sect2>
- <sect2 id="tac_elim">
+ </sect1>
+ <sect1 id="tac_elim">
<title>elim <term> [using <term>] [<intros_spec>]</title>
<para><userinput>elim t using th hyps</userinput></para>
<para>
</varlistentry>
</variablelist>
</para>
- </sect2>
- <sect2 id="tac_elimType">
+ </sect1>
+ <sect1 id="tac_elimType">
<title>elimType <term> [using <term>]</title>
<para><userinput>elimType T using th</userinput></para>
<para>
</varlistentry>
</variablelist>
</para>
- </sect2>
- <sect2 id="tac_exact">
+ </sect1>
+ <sect1 id="tac_exact">
<title>exact <term></title>
<para><userinput>exact p</userinput></para>
<para>
</varlistentry>
</variablelist>
</para>
- </sect2>
- <sect2 id="tac_exists">
+ </sect1>
+ <sect1 id="tac_exists">
<title>exists</title>
- <para><userinput>exists</userinput></para>
+ <para><userinput>exists </userinput></para>
<para>
<variablelist>
<varlistentry>
</varlistentry>
</variablelist>
</para>
- </sect2>
- <sect2 id="tac_fail">
- <title>fail</title>
+ </sect1>
+ <sect1 id="tac_fail">
+ <title>fail </title>
<para><userinput>fail</userinput></para>
<para>
<variablelist>
</varlistentry>
</variablelist>
</para>
- </sect2>
- <sect2 id="tac_fold">
+ </sect1>
+ <sect1 id="tac_fold">
<title>fold <reduction_kind> <term> <pattern></title>
<para><userinput>fold red t patt</userinput></para>
<para>
</varlistentry>
</variablelist>
</para>
- </sect2>
- <sect2 id="tac_fourier">
+ </sect1>
+ <sect1 id="tac_fourier">
<title>fourier</title>
- <para><userinput>fourier</userinput></para>
+ <para><userinput>fourier </userinput></para>
<para>
<variablelist>
<varlistentry>
</varlistentry>
</variablelist>
</para>
- </sect2>
- <sect2 id="tac_fwd">
+ </sect1>
+ <sect1 id="tac_fwd">
<title>fwd <ident> [<ident list>]</title>
<para><userinput>fwd ...TODO</userinput></para>
<para>
</varlistentry>
</variablelist>
</para>
- </sect2>
- <sect2 id="tac_generalize">
+ </sect1>
+ <sect1 id="tac_generalize">
<title>generalize <pattern> [as <id>]</title>
<para>The tactic <command>generalize</command> </para>
- </sect2>
- <sect2 id="tac_id">
+ </sect1>
+ <sect1 id="tac_id">
<title>id</title>
<para>The tactic <command>id</command> </para>
- </sect2>
- <sect2 id="tac_injection">
+ </sect1>
+ <sect1 id="tac_injection">
<title>injection <term></title>
<para>The tactic <command>injection</command> </para>
- </sect2>
- <sect2 id="tac_intro">
+ </sect1>
+ <sect1 id="tac_intro">
<title>intro [<ident>]</title>
<para>The tactic <command>intro</command> </para>
- </sect2>
- <sect2 id="tac_intros">
+ </sect1>
+ <sect1 id="tac_intros">
<title>intros <intros_spec></title>
<para>The tactic <command>intros</command> </para>
- </sect2>
- <sect2 id="tac_inversion">
+ </sect1>
+ <sect1 id="tac_inversion">
<title>intros <term></title>
<para>The tactic <command>intros</command> </para>
- </sect2>
- <sect2 id="tac_lapply">
+ </sect1>
+ <sect1 id="tac_lapply">
<title>lapply [depth=<int>] <term> [to <term list] [using <ident>]</title>
<para>The tactic <command>lapply</command> </para>
- </sect2>
- <sect2 id="tac_left">
+ </sect1>
+ <sect1 id="tac_left">
<title>left</title>
<para>The tactic <command>left</command> </para>
- </sect2>
- <sect2 id="tac_letin">
+ </sect1>
+ <sect1 id="tac_letin">
<title>letin <ident> ≝ <term></title>
<para>The tactic <command>letin</command> </para>
- </sect2>
- <sect2 id="tac_normalize">
+ </sect1>
+ <sect1 id="tac_normalize">
<title>normalize <pattern></title>
<para>The tactic <command>normalize</command> </para>
- </sect2>
- <sect2 id="tac_paramodulation">
+ </sect1>
+ <sect1 id="tac_paramodulation">
<title>paramodulation <pattern></title>
<para>The tactic <command>paramodulation</command> </para>
- </sect2>
- <sect2 id="tac_reduce">
+ </sect1>
+ <sect1 id="tac_reduce">
<title>reduce <pattern></title>
<para>The tactic <command>reduce</command> </para>
- </sect2>
- <sect2 id="tac_reflexivity">
+ </sect1>
+ <sect1 id="tac_reflexivity">
<title>reflexivity</title>
<para>The tactic <command>reflexivity</command> </para>
- </sect2>
- <sect2 id="tac_replace">
+ </sect1>
+ <sect1 id="tac_replace">
<title>replace <pattern> with <term></title>
<para>The tactic <command>replace</command> </para>
- </sect2>
- <sect2 id="tac_rewrite">
+ </sect1>
+ <sect1 id="tac_rewrite">
<title>rewrite {<|>} <term> <pattern></title>
<para>The tactic <command>rewrite</command> </para>
- </sect2>
- <sect2 id="tac_right">
+ </sect1>
+ <sect1 id="tac_right">
<title>right</title>
<para>The tactic <command>right</command> </para>
- </sect2>
- <sect2 id="tac_ring">
+ </sect1>
+ <sect1 id="tac_ring">
<title>ring</title>
<para>The tactic <command>ring</command> </para>
- </sect2>
- <sect2 id="tac_simplify">
+ </sect1>
+ <sect1 id="tac_simplify">
<title>simplify <pattern></title>
<para>The tactic <command>simplify</command> </para>
- </sect2>
- <sect2 id="tac_split">
+ </sect1>
+ <sect1 id="tac_split">
<title>split</title>
<para>The tactic <command>split</command> </para>
- </sect2>
- <sect2 id="tac_symmetry">
+ </sect1>
+ <sect1 id="tac_symmetry">
<title>symmetry</title>
<para>The tactic <command>symmetry</command> </para>
- </sect2>
- <sect2 id="tac_transitivity">
+ </sect1>
+ <sect1 id="tac_transitivity">
<title>transitivity <term></title>
<para>The tactic <command>transitivity</command> </para>
- </sect2>
- <sect2 id="tac_unfold">
+ </sect1>
+ <sect1 id="tac_unfold">
<title>unfold [<term>] <pattern></title>
<para>The tactic <command>unfold</command> </para>
- </sect2>
- <sect2 id="tac_whd">
+ </sect1>
+ <sect1 id="tac_whd">
<title>whd <pattern></title>
<para>The tactic <command>whd</command> </para>
- </sect2>
+ </sect1>
-</sect1>
+</chapter>