1 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
6 <entry id="grammar.tactic">&tactic;</entry>
8 <entry><link linkend="tac_absurd"><emphasis role="bold">absurd</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
13 <entry><link linkend="tac_apply"><emphasis role="bold">apply</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
18 <entry><link linkend="tac_applyS"><emphasis role="bold">applyS</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis></entry>
24 <link linkend="tac_assumption">
25 <emphasis role="bold">assumption</emphasis>
32 <entry><link linkend="tac_auto"><emphasis role="bold">auto</emphasis></link> <emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis></entry>
38 <link linkend="tac_cases"><emphasis role="bold">cases</emphasis></link>
39 <emphasis><link linkend="grammar.term">term</link></emphasis> [<emphasis role="bold">(</emphasis>[<emphasis><link linkend="grammar.id">id</link></emphasis>]…<emphasis role="bold">)</emphasis>]
45 <entry><link linkend="tac_change"><emphasis role="bold">change</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> <emphasis role="bold">with</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
51 <link linkend="tac_clear"><emphasis role="bold">clear</emphasis></link>
52 <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis><link linkend="grammar.id">id</link></emphasis>…]
58 <entry><link linkend="tac_clearbody"><emphasis role="bold">clearbody</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis></entry>
63 <entry><link linkend="tac_constructor"><emphasis role="bold">constructor</emphasis></link> <emphasis><link linkend="grammar.nat">nat</link></emphasis></entry>
69 <link linkend="tac_contradiction">
70 <emphasis role="bold">contradiction</emphasis>
77 <entry><link linkend="tac_cut"><emphasis role="bold">cut</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]</entry>
83 <link linkend="tac_decompose"><emphasis role="bold">decompose</emphasis></link>
84 [<emphasis role="bold">(</emphasis>
85 <emphasis><link linkend="grammar.id">id</link></emphasis>…
86 <emphasis role="bold">)</emphasis>]
87 [<emphasis><link linkend="grammar.id">id</link></emphasis>]
88 [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>…]
95 <link linkend="tac_demodulate">
96 <emphasis role="bold">demodulate</emphasis>
103 <entry><link linkend="tac_destruct"><emphasis role="bold">destruct</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
108 <entry><link linkend="tac_elim"><emphasis role="bold">elim</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis role="bold">using</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>] <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></entry>
113 <entry><link linkend="tac_elimType"><emphasis role="bold">elimType</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis role="bold">using</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>] <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></entry>
118 <entry><link linkend="tac_exact"><emphasis role="bold">exact</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
124 <link linkend="tac_exists">
125 <emphasis role="bold">exists</emphasis>
133 <link linkend="tac_fail">
134 <emphasis role="bold">fail</emphasis>
141 <entry><link linkend="tac_fold"><emphasis role="bold">fold</emphasis></link> <emphasis><link linkend="grammar.reduction-kind">reduction-kind</link></emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
147 <link linkend="tac_fourier">
148 <emphasis role="bold">fourier</emphasis>
155 <entry><link linkend="tac_fwd"><emphasis role="bold">fwd</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis><link linkend="grammar.id">id</link></emphasis>]…]</entry>
160 <entry><link linkend="tac_generalize"><emphasis role="bold">generalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]</entry>
166 <link linkend="tac_id">
167 <emphasis role="bold">id</emphasis>
174 <entry><link linkend="tac_intro"><emphasis role="bold">intro</emphasis></link> [<emphasis><link linkend="grammar.id">id</link></emphasis>]</entry>
179 <entry><link linkend="tac_intros"><emphasis role="bold">intros</emphasis></link> <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></entry>
184 <entry><link linkend="tac_inversion"><emphasis role="bold">inversion</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
190 <link linkend="tac_lapply"><emphasis role="bold">lapply</emphasis></link>
191 [<emphasis role="bold">linear</emphasis>]
192 [<emphasis role="bold">depth=</emphasis><emphasis><link linkend="grammar.nat">nat</link></emphasis>]
193 <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>
194 [<emphasis role="bold">to</emphasis>
195 <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>
196 [<emphasis role="bold">,</emphasis><emphasis><link linkend="grammar.sterm">sterm</link></emphasis>…]
198 [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]
205 <link linkend="tac_left">
206 <emphasis role="bold">left</emphasis>
213 <entry><link linkend="tac_letin"><emphasis role="bold">letin</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold">≝</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
218 <entry><link linkend="tac_normalize"><emphasis role="bold">normalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
223 <entry><link linkend="tac_reduce"><emphasis role="bold">reduce</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
229 <link linkend="tac_reflexivity">
230 <emphasis role="bold">reflexivity</emphasis>
237 <entry><link linkend="tac_replace"><emphasis role="bold">replace</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> <emphasis role="bold">with</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
242 <entry><link linkend="tac_rewrite"><emphasis role="bold">rewrite</emphasis></link> [<emphasis role="bold"><</emphasis>|<emphasis role="bold">></emphasis>] <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
248 <link linkend="tac_right">
249 <emphasis role="bold">right</emphasis>
257 <link linkend="tac_ring">
258 <emphasis role="bold">ring</emphasis>
265 <entry><link linkend="tac_simplify"><emphasis role="bold">simplify</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
271 <link linkend="tac_split">
272 <emphasis role="bold">split</emphasis>
280 <link linkend="tac_subst">
281 <emphasis role="bold">subst</emphasis>
289 <link linkend="tac_symmetry">
290 <emphasis role="bold">symmetry</emphasis>
297 <entry><link linkend="tac_transitivity"><emphasis role="bold">transitivity</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
302 <entry><link linkend="tac_unfold"><emphasis role="bold">unfold</emphasis></link> [<emphasis><link linkend="grammar.sterm">sterm</link></emphasis>] <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
307 <entry><link linkend="tac_whd"><emphasis role="bold">whd</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>