<title>Tactics</title>
<sect1 id="tac_absurd">
- <title>absurd <term></title>
+ <title>absurd &term;</title>
<titleabbrev>absurd</titleabbrev>
<para><userinput>absurd P</userinput></para>
<para>
</para>
</sect1>
<sect1 id="tac_apply">
- <title>apply <term></title>
+ <title>apply &term;</title>
<titleabbrev>apply</titleabbrev>
<para><userinput>apply t</userinput></para>
<para>
</para>
</sect1>
<sect1 id="tac_auto">
- <title>auto [depth=<int>] [width=<int>] [paramodulation] [full]</title>
+ <title>auto [depth=&nat;] [width=&nat;] [paramodulation] [full]</title>
<titleabbrev>auto</titleabbrev>
<para><userinput>auto depth=d width=w paramodulation full</userinput></para>
<para>
</para>
</sect1>
<sect1 id="tac_clear">
- <title>clear <id></title>
+ <title>clear &id;</title>
<titleabbrev>clear</titleabbrev>
<para><userinput>clear H</userinput></para>
<para>
</para>
</sect1>
<sect1 id="tac_clearbody">
- <title>clearbody <id></title>
+ <title>clearbody &id;</title>
<titleabbrev>clearbody</titleabbrev>
<para><userinput>clearbody H</userinput></para>
<para>
</para>
</sect1>
<sect1 id="tac_change">
- <title>change <pattern> with <term></title>
+ <title>change <pattern> with &term;</title>
<titleabbrev>change</titleabbrev>
<para><userinput>change patt with t</userinput></para>
<para>
</para>
</sect1>
<sect1 id="tac_constructor">
- <title>constructor <int></title>
+ <title>constructor &nat;</title>
<titleabbrev>constructor</titleabbrev>
<para><userinput>constructor n</userinput></para>
<para>
</para>
</sect1>
<sect1 id="tac_cut">
- <title>cut <term> [as <id>]</title>
+ <title>cut &term; [as &id;]</title>
<titleabbrev>cut</titleabbrev>
<para><userinput>cut P as H</userinput></para>
<para>
</para>
</sect1>
<sect1 id="tac_decompose">
- <title>decompose [<ident list>] <ident> [<intros_spec>]</title>
+ <title>decompose &id; [&id;]… [<intros_spec>]</title>
<titleabbrev>decompose</titleabbrev>
<para><userinput>decompose ???</userinput></para>
<para>
</para>
</sect1>
<sect1 id="tac_discriminate">
- <title>discriminate <term></title>
+ <title>discriminate &term;</title>
<titleabbrev>discriminate</titleabbrev>
<para><userinput>discriminate p</userinput></para>
<para>
</para>
</sect1>
<sect1 id="tac_elim">
- <title>elim <term> [using <term>] [<intros_spec>]</title>
+ <title>elim &term; [using &term;] [<intros_spec>]</title>
<titleabbrev>elim</titleabbrev>
<para><userinput>elim t using th hyps</userinput></para>
<para>
</para>
</sect1>
<sect1 id="tac_elimType">
- <title>elimType <term> [using <term>] [<intros_spec>]</title>
+ <title>elimType &term; [using &term;] [<intros_spec>]</title>
<titleabbrev>elimType</titleabbrev>
<para><userinput>elimType T using th hyps</userinput></para>
<para>
</para>
</sect1>
<sect1 id="tac_exact">
- <title>exact <term></title>
+ <title>exact &term;</title>
<titleabbrev>exact</titleabbrev>
<para><userinput>exact p</userinput></para>
<para>
</para>
</sect1>
<sect1 id="tac_fold">
- <title>fold <reduction_kind> <term> <pattern></title>
+ <title>fold <reduction_kind> &term; <pattern></title>
<titleabbrev>fold</titleabbrev>
<para><userinput>fold red t patt</userinput></para>
<para>
</para>
</sect1>
<sect1 id="tac_fwd">
- <title>fwd <ident> [<ident list>]</title>
+ <title>fwd &id; [<ident list>]</title>
<titleabbrev>fwd</titleabbrev>
<para><userinput>fwd ...TODO</userinput></para>
<para>
</para>
</sect1>
<sect1 id="tac_generalize">
- <title>generalize <pattern> [as <id>]</title>
+ <title>generalize <pattern> [as &id;]</title>
<titleabbrev>generalize</titleabbrev>
<para><userinput>generalize patt as H</userinput></para>
<para>
</para>
</sect1>
<sect1 id="tac_injection">
- <title>injection <term></title>
+ <title>injection &term;</title>
<titleabbrev>injection</titleabbrev>
<para><userinput>injection p</userinput></para>
<para>
</para>
</sect1>
<sect1 id="tac_intro">
- <title>intro [<ident>]</title>
+ <title>intro [&id;]</title>
<titleabbrev>intro</titleabbrev>
<para><userinput>intro H</userinput></para>
<para>
</para>
</sect1>
<sect1 id="tac_inversion">
- <title>inversion <term></title>
+ <title>inversion &term;</title>
<titleabbrev>inversion</titleabbrev>
<para><userinput>inversion t</userinput></para>
<para>
</para>
</sect1>
<sect1 id="tac_lapply">
- <title>lapply [depth=<int>] <term> [to <term list] [using <ident>]</title>
+ <title>lapply [depth=&nat;] &term; [to <term list>] [using &id;]</title>
<titleabbrev>lapply</titleabbrev>
<para><userinput>lapply ???</userinput></para>
<para>
</para>
</sect1>
<sect1 id="tac_letin">
- <title>letin <ident> ≝ <term></title>
+ <title>letin &id; ≝ &term;</title>
<titleabbrev>letin</titleabbrev>
<para><userinput>letin x ≝ t</userinput></para>
<para>
</para>
</sect1>
<sect1 id="tac_replace">
- <title>replace <pattern> with <term></title>
+ <title>replace <pattern> with &term;</title>
<titleabbrev>change</titleabbrev>
<para><userinput>change patt with t</userinput></para>
<para>
</para>
</sect1>
<sect1 id="tac_rewrite">
- <title>rewrite {<|>} <term> <pattern></title>
+ <title>rewrite [<|>] &term; <pattern></title>
<titleabbrev>rewrite</titleabbrev>
<para><userinput>rewrite dir p patt</userinput></para>
<para>
</para>
</sect1>
<sect1 id="tac_transitivity">
- <title>transitivity <term></title>
+ <title>transitivity &term;</title>
<titleabbrev>transitivity</titleabbrev>
<para><userinput>transitivity t</userinput></para>
<para>
</para>
</sect1>
<sect1 id="tac_unfold">
- <title>unfold [<term>] <pattern></title>
+ <title>unfold [&term;] <pattern></title>
<titleabbrev>unfold</titleabbrev>
<para><userinput>unfold t patt</userinput></para>
<para>