<row>
<entry id="grammar.tactic">&tactic;</entry>
<entry>::=</entry>
- <entry>
- <link linkend="tac_#">
- <emphasis role="bold">#</emphasis>
- </link>
- <emphasis>
- <link linkend="grammar.id">id</link>
- </emphasis>
- </entry>
+ <entry><emphasis role="bold">@</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry>
- <link linkend="tac_##">
- <emphasis role="bold">##</emphasis>
- </link>
- </entry>
+ <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>
</row>
<row>
<entry/>
<entry>|</entry>
<entry>
- <link linkend="tac_#_">
- <emphasis role="bold">#_</emphasis>
+ <link linkend="tac_assumption">
+ <emphasis role="bold">assumption</emphasis>
</link>
</entry>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry><link linkend="tac_%"><emphasis role="bold">%</emphasis></link> [<emphasis><link linkend="grammar.nat">nat</link></emphasis>] [<emphasis role="bol">{</emphasis><emphasis><link linkend="grammar.sterm">sterm</link></emphasis>…<emphasis role="bol">}</emphasis>]</entry>
- </row>
- <row>
- <entry/>
- <entry>|</entry>
- <entry>
- <link linkend="tac_*"><emphasis role="bold">*</emphasis></link>
- [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]
- </entry>
+ <entry><emphasis role="bold">/</emphasis><emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis><emphasis role="bold">/</emphasis>. </entry>
</row>
<row>
<entry/>
<entry>|</entry>
<entry>
- <link linkend="tac_-"><emphasis role="bold">-</emphasis></link><emphasis><link linkend="grammar.id">id</link></emphasis>
+ <link linkend="tac_cases"><emphasis role="bold">cases</emphasis></link>
+ <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis>
</entry>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry><emphasis role="bold">/</emphasis><emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis><emphasis role="bold">/</emphasis>. </entry>
- </row>
- <row>
- <entry/>
- <entry>|</entry>
- <entry>[<emphasis role="bold"><</emphasis>|<link linkend="tac_>"><emphasis role="bold">></emphasis></link>] <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
+ <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>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry><link linkend="tac_@"><emphasis role="bold">@</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
+ <entry>
+ <emphasis role="bold">-</emphasis><emphasis><link linkend="grammar.id">id</link></emphasis>
+ </entry>
</row>
<row>
<entry/>
<entry>|</entry>
- <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>
+ <entry><emphasis role="bold">%</emphasis> [<emphasis><link linkend="grammar.nat">nat</link></emphasis>] [<emphasis role="bol">{</emphasis><emphasis><link linkend="grammar.sterm">sterm</link></emphasis>…<emphasis role="bol">}</emphasis>]</entry>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry>
- <link linkend="tac_assumption">
- <emphasis role="bold">assumption</emphasis>
- </link>
- </entry>
+ <entry><link linkend="tac_cut"><emphasis role="bold">cut</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
</row>
<row>
<entry/>
<entry>|</entry>
<entry>
- <link linkend="tac_cases"><emphasis role="bold">cases</emphasis></link>
- <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis>
+ <emphasis role="bold">*</emphasis>
+ [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]
</entry>
</row>
<row>
<entry/>
<entry>|</entry>
- <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>
+ <entry><link linkend="tac_destruct"><emphasis role="bold">destruct</emphasis></link>
+ [<emphasis role="bold">(</emphasis><emphasis><link linkend="grammar.id">id</link></emphasis>…<emphasis role="bold">)</emphasis>] [<emphasis role="bold">skip</emphasis> <emphasis role="bold">(</emphasis><emphasis><link linkend="grammar.id">id</link></emphasis>…<emphasis role="bold">)</emphasis>]</entry>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry><link linkend="tac_cut"><emphasis role="bold">cut</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
+ <entry><link linkend="tac_elim"><emphasis role="bold">elim</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry><link linkend="tac_destruct"><emphasis role="bold">destruct</emphasis></link>
- [<emphasis role="bold">(</emphasis><emphasis><link linkend="grammar.id">id</link></emphasis>…<emphasis role="bold">)</emphasis>] [<emphasis role="bold">skip</emphasis> <emphasis role="bold">(</emphasis><emphasis><link linkend="grammar.id">id</link></emphasis>…<emphasis role="bold">)</emphasis>]</entry>
+ <entry><link linkend="tac_generalize"><emphasis role="bold">generalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry><link linkend="tac_elim"><emphasis role="bold">elim</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
+ <entry>
+ <emphasis role="bold">#</emphasis>
+ <emphasis>
+ <link linkend="grammar.id">id</link>
+ </emphasis>
+ </entry>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry><link linkend="tac_generalize"><emphasis role="bold">generalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
+ <entry>
+ <emphasis role="bold">#_</emphasis>
+ </entry>
</row>
<row>
<entry/>
<entry>|</entry>
<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>
</row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry>
+ <emphasis role="bold">##</emphasis>
+ </entry>
+ </row>
<row>
<entry/>
<entry>|</entry>
<entry><link linkend="tac_normalize"><emphasis role="bold">normalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis>
[<emphasis role="bold">nodelta</emphasis>]</entry>
</row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry>[<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>
+ </row>
<row>
<entry/>
<entry>|</entry>