1 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
6 <entry id="grammar.declarative_tactic">&tactic;</entry>
9 <link linkend="tac_rewrite_step"><emphasis role="bold">=</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis> [<emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis> | <emphasis role="bold">using</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> | <emphasis role="bold">using once</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> | <emphasis role="bold">proof</emphasis>] [<emphasis role="bold">done</emphasis>]
15 <entry><link linkend="tac_assume"><emphasis role="bold">assume</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold"> : </emphasis>
16 <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> </entry>
21 <entry><link linkend="tac_byinduction"><emphasis role="bold">by induction hypothesis we know</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold"> (</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold">)</emphasis></entry>
26 <entry><link linkend="tac_case"><emphasis role="bold">case</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis role="bold">(</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold">:</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold">)</emphasis>] … [<emphasis role="bold">(</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold">:</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold">)</emphasis>]</entry>
31 <entry><link linkend="tac_conclude"><emphasis role="bold">conclude</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis></entry>
36 <entry><emphasis><link linkend="grammar.justification">justification</link></emphasis> <link linkend="tac_bydone"><emphasis role="bold">done</emphasis></link></entry>
41 <entry><emphasis><link linkend="grammar.justification">justification</link></emphasis> <emphasis role="bold">let</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>
42 <emphasis role="bold">:</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold">such that</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis>
43 <emphasis role="bold">(</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold">)</emphasis></entry>
48 <entry><emphasis role="bold">let</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold"> = </emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis></entry>
53 <entry><link linkend="tac_obtain"><emphasis role="bold">obtain</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis></entry>
58 <entry><link linkend="tac_suppose"><emphasis role="bold">suppose</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold"> (</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>
59 <emphasis role="bold">) </emphasis></entry>
65 <link linkend="tac_thatisequivalentto"><emphasis role="bold">that is equivalent to</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis>
71 <entry><link linkend="tac_thesisbecomes"><emphasis role="bold">the thesis becomes</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis> </entry>
76 <entry><link linkend="tac_weneedtoprove"><emphasis role="bold">we need to prove</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis>
77 [<emphasis role="bold">(</emphasis><emphasis><link linkend="grammar.id">id</link></emphasis>
78 <emphasis role="bold">)</emphasis>]
84 <entry><link linkend="tac_weproceedbycases"><emphasis role="bold">we proceed by cases on</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold">to prove</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> </entry>
89 <entry><link linkend="tac_weproceedbyinduction"><emphasis role="bold">we proceed by induction on</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold"> to prove </emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> </entry>
94 <entry><emphasis><link linkend="grammar.justification">justification</link></emphasis> <link linkend="tac_bytermweproved"><emphasis role="bold">we proved</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis>
95 [<emphasis role="bold">(</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>
96 <emphasis role="bold">)</emphasis>]