2 <!-- ============ Tactics ====================== -->
6 <sect2 id="tac_absurd">
7 <title>absurd <term></title>
8 <para>The tactic <command>absurd</command> </para>
12 <sect2 id="tac_apply">
13 <title>apply <term></title>
14 <para>The tactic <command>apply</command> </para>
16 <sect2 id="tac_assumption">
17 <title>assumption</title>
18 <para>The tactic <command>assumption</command> </para>
21 <title>auto [depth=<int>] [width=<int>] [paramodulation] [full]</title>
22 <para>The tactic <command>auto</command> </para>
24 <sect2 id="tac_clear">
25 <title>clear <id></title>
26 <para>The tactic <command>clear</command> </para>
28 <sect2 id="tac_clearbody">
29 <title>clearbody <id></title>
30 <para>The tactic <command>clearbody</command> </para>
32 <sect2 id="tac_change">
33 <title>change <pattern> with <term></title>
34 <para>The tactic <command>change</command> </para>
36 <sect2 id="tac_compare">
37 <title>compare <term></title>
38 <para>The tactic <command>compare</command> </para>
40 <sect2 id="tac_constructor">
41 <title>constructor <int></title>
42 <para>The tactic <command>constructor</command> </para>
44 <sect2 id="tac_contradiction">
45 <title>contradiction</title>
46 <para>The tactic <command>contradiction</command> </para>
49 <title>cut <term> [as <id>]</title>
50 <para>The tactic <command>cut</command> </para>
52 <sect2 id="tac_decide_equality">
54 <para>The tactic <command>decide equality</command> </para>
56 <sect2 id="tac_decompose">
57 <title>decompose [<ident list>] <ident> [<intros_spec>]</title>
58 <para>The tactic <command>decompose</command> </para>
60 <sect2 id="tac_discriminate">
61 <title>discriminate <term></title>
62 <para>The tactic <command>discriminate</command> </para>
65 <title>elim <term> [using <term>] [<intros_spec>]</title>
66 <para>The tactic <command>elim</command> </para>
68 <sect2 id="tac_elimType">
69 <title>elimType <term> [using <term>]</title>
70 <para>The tactic <command>elimType</command> </para>
72 <sect2 id="tac_exact">
73 <title>exact <term></title>
74 <para>The tactic <command>exact</command> </para>
76 <sect2 id="tac_exists">
78 <para>The tactic <command>exists</command> </para>
82 <para>The tactic <command>fail</command> </para>
85 <title>fold <reduction_kind> <term> <pattern></title>
86 <para>The tactic <command>fold</command> </para>
88 <sect2 id="tac_fourier">
89 <title>fourier</title>
90 <para>The tactic <command>fourier</command> </para>
93 <title>fwd <ident> [<ident list>]</title>
94 <para>The tactic <command>fwd</command> </para>
96 <sect2 id="tac_generalize">
97 <title>generalize <pattern> [as <id>]</title>
98 <para>The tactic <command>generalize</command> </para>
102 <para>The tactic <command>id</command> </para>
104 <sect2 id="tac_injection">
105 <title>injection <term></title>
106 <para>The tactic <command>injection</command> </para>
108 <sect2 id="tac_intro">
109 <title>intro [<ident>]</title>
110 <para>The tactic <command>intro</command> </para>
112 <sect2 id="tac_intros">
113 <title>intros <intros_spec></title>
114 <para>The tactic <command>intros</command> </para>
116 <sect2 id="tac_inversion">
117 <title>intros <term></title>
118 <para>The tactic <command>intros</command> </para>
120 <sect2 id="tac_lapply">
121 <title>lapply [depth=<int>] <term> [to <term list] [using <ident>]</title>
122 <para>The tactic <command>lapply</command> </para>
124 <sect2 id="tac_left">
126 <para>The tactic <command>left</command> </para>
128 <sect2 id="tac_letin">
129 <title>letin <ident> ≝ <term></title>
130 <para>The tactic <command>letin</command> </para>
132 <sect2 id="tac_normalize">
133 <title>normalize <pattern></title>
134 <para>The tactic <command>normalize</command> </para>
136 <sect2 id="tac_paramodulation">
137 <title>paramodulation <pattern></title>
138 <para>The tactic <command>paramodulation</command> </para>
140 <sect2 id="tac_reduce">
141 <title>reduce <pattern></title>
142 <para>The tactic <command>reduce</command> </para>
144 <sect2 id="tac_reflexivity">
145 <title>reflexivity</title>
146 <para>The tactic <command>reflexivity</command> </para>
148 <sect2 id="tac_replace">
149 <title>replace <pattern> with <term></title>
150 <para>The tactic <command>replace</command> </para>
152 <sect2 id="tac_rewrite">
153 <title>rewrite {<|>} <term> <pattern></title>
154 <para>The tactic <command>rewrite</command> </para>
156 <sect2 id="tac_right">
158 <para>The tactic <command>right</command> </para>
160 <sect2 id="tac_ring">
162 <para>The tactic <command>ring</command> </para>
164 <sect2 id="tac_simplify">
165 <title>simplify <pattern></title>
166 <para>The tactic <command>simplify</command> </para>
168 <sect2 id="tac_split">
170 <para>The tactic <command>split</command> </para>
172 <sect2 id="tac_symmetry">
173 <title>symmetry</title>
174 <para>The tactic <command>symmetry</command> </para>
176 <sect2 id="tac_transitivity">
177 <title>transitivity <term></title>
178 <para>The tactic <command>transitivity</command> </para>
180 <sect2 id="tac_unfold">
181 <title>unfold [<term>] <pattern></title>
182 <para>The tactic <command>unfold</command> </para>
185 <title>whd <pattern></title>
186 <para>The tactic <command>whd</command> </para>