<sect1 id="tactics">
<title>Tactics</title>
- <sect2 id="absurd">
+ <sect2 id="tac_absurd">
<title>absurd <term></title>
<para>The tactic <command>absurd</command> </para>
<para>
<ulink url="#terms">ciao</ulink>
</para>
</sect2>
- <sect2 id="apply">
+ <sect2 id="tac_apply">
<title>apply <term></title>
<para>The tactic <command>apply</command> </para>
</sect2>
- <sect2 id="assumption">
+ <sect2 id="tac_assumption">
<title>assumption</title>
<para>The tactic <command>assumption</command> </para>
</sect2>
- <sect2 id="auto">
+ <sect2 id="tac_auto">
<title>auto [depth=<int>] [width=<int>] [paramodulation] [full]</title>
<para>The tactic <command>auto</command> </para>
</sect2>
- <sect2 id="clear">
+ <sect2 id="tac_clear">
<title>clear <id></title>
<para>The tactic <command>clear</command> </para>
</sect2>
- <sect2 id="clearbody">
+ <sect2 id="tac_clearbody">
<title>clearbody <id></title>
<para>The tactic <command>clearbody</command> </para>
</sect2>
- <sect2 id="change">
+ <sect2 id="tac_change">
<title>change <pattern> with <term></title>
<para>The tactic <command>change</command> </para>
</sect2>
- <sect2 id="compare">
+ <sect2 id="tac_compare">
<title>compare <term></title>
<para>The tactic <command>compare</command> </para>
</sect2>
- <sect2 id="constructor">
+ <sect2 id="tac_constructor">
<title>constructor <int></title>
<para>The tactic <command>constructor</command> </para>
</sect2>
- <sect2 id="contradiction">
+ <sect2 id="tac_contradiction">
<title>contradiction</title>
<para>The tactic <command>contradiction</command> </para>
</sect2>
- <sect2 id="cut">
+ <sect2 id="tac_cut">
<title>cut <term> [as <id>]</title>
<para>The tactic <command>cut</command> </para>
</sect2>
- <sect2 id="decide equality">
+ <sect2 id="tac_decide equality">
<title>decide</title>
<para>The tactic <command>decide equality</command> </para>
</sect2>
- <sect2 id="decompose">
+ <sect2 id="tac_decompose">
<title>decompose [<ident list>] <ident> [<intros_spec>]</title>
<para>The tactic <command>decompose</command> </para>
</sect2>
- <sect2 id="discriminate">
+ <sect2 id="tac_discriminate">
<title>discriminate <term></title>
<para>The tactic <command>discriminate</command> </para>
</sect2>
- <sect2 id="elim">
+ <sect2 id="tac_elim">
<title>elim <term> [using <term>] [<intros_spec>]</title>
<para>The tactic <command>elim</command> </para>
</sect2>
- <sect2 id="elimType">
+ <sect2 id="tac_elimType">
<title>elimType <term> [using <term>]</title>
<para>The tactic <command>elimType</command> </para>
</sect2>
- <sect2 id="exact">
+ <sect2 id="tac_exact">
<title>exact <term></title>
<para>The tactic <command>exact</command> </para>
</sect2>
- <sect2 id="exists">
+ <sect2 id="tac_exists">
<title>exists</title>
<para>The tactic <command>exists</command> </para>
</sect2>
- <sect2 id="fail">
+ <sect2 id="tac_fail">
<title>fail</title>
<para>The tactic <command>fail</command> </para>
</sect2>
- <sect2 id="fold">
+ <sect2 id="tac_fold">
<title>fold <reduction_kind> <term> <pattern></title>
<para>The tactic <command>fold</command> </para>
</sect2>
- <sect2 id="fourier">
+ <sect2 id="tac_fourier">
<title>fourier</title>
<para>The tactic <command>fourier</command> </para>
</sect2>
- <sect2 id="fwd">
+ <sect2 id="tac_fwd">
<title>fwd <ident> [<ident list>]</title>
<para>The tactic <command>fwd</command> </para>
</sect2>
- <sect2 id="generalize">
+ <sect2 id="tac_generalize">
<title>generalize <pattern> [as <id>]</title>
<para>The tactic <command>generalize</command> </para>
</sect2>
- <sect2 id="id">
+ <sect2 id="tac_id">
<title>id</title>
<para>The tactic <command>id</command> </para>
</sect2>
- <sect2 id="injection">
+ <sect2 id="tac_injection">
<title>injection <term></title>
<para>The tactic <command>injection</command> </para>
</sect2>
- <sect2 id="intro">
+ <sect2 id="tac_intro">
<title>intro [<ident>]</title>
<para>The tactic <command>intro</command> </para>
</sect2>
- <sect2 id="intros">
+ <sect2 id="tac_intros">
<title>intros <intros_spec></title>
<para>The tactic <command>intros</command> </para>
</sect2>
- <sect2 id="inversion">
+ <sect2 id="tac_inversion">
<title>intros <term></title>
<para>The tactic <command>intros</command> </para>
</sect2>
- <sect2 id="lapply">
+ <sect2 id="tac_lapply">
<title>lapply [depth=<int>] <term> [to <term list] [using <ident>]</title>
<para>The tactic <command>lapply</command> </para>
</sect2>
- <sect2 id="left">
+ <sect2 id="tac_left">
<title>left</title>
<para>The tactic <command>left</command> </para>
</sect2>
- <sect2 id="letin">
+ <sect2 id="tac_letin">
<title>letin <ident> ≝ <term></title>
<para>The tactic <command>letin</command> </para>
</sect2>
- <sect2 id="normalize">
+ <sect2 id="tac_normalize">
<title>normalize <pattern></title>
<para>The tactic <command>normalize</command> </para>
</sect2>
- <sect2 id="paramodulation">
+ <sect2 id="tac_paramodulation">
<title>paramodulation <pattern></title>
<para>The tactic <command>paramodulation</command> </para>
</sect2>
- <sect2 id="reduce">
+ <sect2 id="tac_reduce">
<title>reduce <pattern></title>
<para>The tactic <command>reduce</command> </para>
</sect2>
- <sect2 id="reflexivity">
+ <sect2 id="tac_reflexivity">
<title>reflexivity</title>
<para>The tactic <command>reflexivity</command> </para>
</sect2>
- <sect2 id="replace">
+ <sect2 id="tac_replace">
<title>replace <pattern> with <term></title>
<para>The tactic <command>replace</command> </para>
</sect2>
- <sect2 id="rewrite">
+ <sect2 id="tac_rewrite">
<title>rewrite {<|>} <term> <pattern></title>
<para>The tactic <command>rewrite</command> </para>
</sect2>
- <sect2 id="right">
+ <sect2 id="tac_right">
<title>right</title>
<para>The tactic <command>right</command> </para>
</sect2>
- <sect2 id="ring">
+ <sect2 id="tac_ring">
<title>ring</title>
<para>The tactic <command>ring</command> </para>
</sect2>
- <sect2 id="simplify">
+ <sect2 id="tac_simplify">
<title>simplify <pattern></title>
<para>The tactic <command>simplify</command> </para>
</sect2>
- <sect2 id="split">
+ <sect2 id="tac_split">
<title>split</title>
<para>The tactic <command>split</command> </para>
</sect2>
- <sect2 id="symmetry">
+ <sect2 id="tac_symmetry">
<title>symmetry</title>
<para>The tactic <command>symmetry</command> </para>
</sect2>
- <sect2 id="transitivity">
+ <sect2 id="tac_transitivity">
<title>transitivity <term></title>
<para>The tactic <command>transitivity</command> </para>
</sect2>
- <sect2 id="unfold">
+ <sect2 id="tac_unfold">
<title>unfold [<term>] <pattern></title>
<para>The tactic <command>unfold</command> </para>
</sect2>
- <sect2 id="whd">
+ <sect2 id="tac_whd">
<title>whd <pattern></title>
<para>The tactic <command>whd</command> </para>
</sect2>