helm/software/matita/help/C/tactic_quickref.xml

   1 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
   2   <title>tactics</title>
   3   <tgroup cols="3">
   4     <tbody>
   5       <row>
   6         <entry id="grammar.tactic">&tactic;</entry>
   7         <entry>::=</entry>
   8         <entry><link linkend="tac_absurd"><emphasis role="bold">absurd</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
   9       </row>
  10       <row>
  11         <entry/>
  12         <entry>|</entry>
  13         <entry><link linkend="tac_apply"><emphasis role="bold">apply</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
  14       </row>
  15       <row>
  16         <entry/>
  17         <entry>|</entry>
  18         <entry><link linkend="tac_applyS"><emphasis role="bold">applyS</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
  19       </row>
  20       <row>
  21         <entry/>
  22         <entry>|</entry>
  23         <entry>
  24           <link linkend="tac_assumption">
  25             <emphasis role="bold">assumption</emphasis>
  26           </link>
  27         </entry>
  28       </row>
  29       <row>
  30         <entry/>
  31         <entry>|</entry>
  32         <entry><link linkend="tac_auto"><emphasis role="bold">auto</emphasis></link> [<emphasis role="bold">depth=</emphasis><emphasis><link linkend="grammar.nat">nat</link></emphasis>] [<emphasis role="bold">width=</emphasis><emphasis><link linkend="grammar.nat">nat</link></emphasis>] [<emphasis role="bold">paramodulation</emphasis>] [<emphasis role="bold">full</emphasis>]</entry>
  33       </row>
  34       <row>
  35         <entry/>
  36         <entry>|</entry>
  37         <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>
  38       </row>
  39       <row>
  40         <entry/>
  41         <entry>|</entry>
  42         <entry>
  43              <link linkend="tac_clear"><emphasis role="bold">clear</emphasis></link>
  44              <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis><link linkend="grammar.id">id</link></emphasis>…]
  45             </entry>
  46       </row>
  47       <row>
  48         <entry/>
  49         <entry>|</entry>
  50         <entry><link linkend="tac_clearbody"><emphasis role="bold">clearbody</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis></entry>
  51       </row>
  52       <row>
  53         <entry/>
  54         <entry>|</entry>
  55         <entry><link linkend="tac_constructor"><emphasis role="bold">constructor</emphasis></link> <emphasis><link linkend="grammar.nat">nat</link></emphasis></entry>
  56       </row>
  57       <row>
  58         <entry/>
  59         <entry>|</entry>
  60         <entry>
  61           <link linkend="tac_contradiction">
  62             <emphasis role="bold">contradiction</emphasis>
  63           </link>
  64         </entry>
  65       </row>
  66       <row>
  67         <entry/>
  68         <entry>|</entry>
  69         <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>
  70       </row>
  71       <row>
  72         <entry/>
  73         <entry>|</entry>
  74         <entry>
  75              <link linkend="tac_decompose"><emphasis role="bold">decompose</emphasis></link>
  76              [<emphasis role="bold">(</emphasis>
  77              <emphasis><link linkend="grammar.id">id</link></emphasis>…
  78              <emphasis role="bold">)</emphasis>]
  79              [<emphasis><link linkend="grammar.id">id</link></emphasis>]
  80              [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>…]
  81             </entry>
  82       </row>
  83       <row>
  84         <entry/>
  85         <entry>|</entry>
  86         <entry>
  87           <link linkend="tac_demodulate">
  88             <emphasis role="bold">demodulate</emphasis>
  89           </link>
  90         </entry>
  91       </row>
  92       <row>
  93         <entry/>
  94         <entry>|</entry>
  95         <entry><link linkend="tac_discriminate"><emphasis role="bold">discriminate</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
  96       </row>
  97       <row>
  98         <entry/>
  99         <entry>|</entry>
 100         <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>
 101       </row>
 102       <row>
 103         <entry/>
 104         <entry>|</entry>
 105         <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>
 106       </row>
 107       <row>
 108         <entry/>
 109         <entry>|</entry>
 110         <entry><link linkend="tac_exact"><emphasis role="bold">exact</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
 111       </row>
 112       <row>
 113         <entry/>
 114         <entry>|</entry>
 115         <entry>
 116           <link linkend="tac_exists">
 117             <emphasis role="bold">exists</emphasis>
 118           </link>
 119         </entry>
 120       </row>
 121       <row>
 122         <entry/>
 123         <entry>|</entry>
 124         <entry>
 125           <link linkend="tac_fail">
 126             <emphasis role="bold">fail</emphasis>
 127           </link>
 128         </entry>
 129       </row>
 130       <row>
 131         <entry/>
 132         <entry>|</entry>
 133         <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>
 134       </row>
 135       <row>
 136         <entry/>
 137         <entry>|</entry>
 138         <entry>
 139           <link linkend="tac_fourier">
 140             <emphasis role="bold">fourier</emphasis>
 141           </link>
 142         </entry>
 143       </row>
 144       <row>
 145         <entry/>
 146         <entry>|</entry>
 147         <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>
 148       </row>
 149       <row>
 150         <entry/>
 151         <entry>|</entry>
 152         <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>
 153       </row>
 154       <row>
 155         <entry/>
 156         <entry>|</entry>
 157         <entry>
 158           <link linkend="tac_id">
 159             <emphasis role="bold">id</emphasis>
 160           </link>
 161         </entry>
 162       </row>
 163       <row>
 164         <entry/>
 165         <entry>|</entry>
 166         <entry><link linkend="tac_injection"><emphasis role="bold">injection</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
 167       </row>
 168       <row>
 169         <entry/>
 170         <entry>|</entry>
 171         <entry><link linkend="tac_intro"><emphasis role="bold">intro</emphasis></link> [<emphasis><link linkend="grammar.id">id</link></emphasis>]</entry>
 172       </row>
 173       <row>
 174         <entry/>
 175         <entry>|</entry>
 176         <entry><link linkend="tac_intros"><emphasis role="bold">intros</emphasis></link> <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></entry>
 177       </row>
 178       <row>
 179         <entry/>
 180         <entry>|</entry>
 181         <entry><link linkend="tac_inversion"><emphasis role="bold">inversion</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
 182       </row>
 183       <row>
 184         <entry/>
 185         <entry>|</entry>
 186         <entry>
 187              <link linkend="tac_lapply"><emphasis role="bold">lapply</emphasis></link>
 188              [<emphasis role="bold">linear</emphasis>]
 189              [<emphasis role="bold">depth=</emphasis><emphasis><link linkend="grammar.nat">nat</link></emphasis>]
 190              <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>
 191              [<emphasis role="bold">to</emphasis>
 192               <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>
 193               [<emphasis role="bold">,</emphasis><emphasis><link linkend="grammar.sterm">sterm</link></emphasis>…]
 194              ]
 195              [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]
 196             </entry>
 197       </row>
 198       <row>
 199         <entry/>
 200         <entry>|</entry>
 201         <entry>
 202           <link linkend="tac_left">
 203             <emphasis role="bold">left</emphasis>
 204           </link>
 205         </entry>
 206       </row>
 207       <row>
 208         <entry/>
 209         <entry>|</entry>
 210         <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>
 211       </row>
 212       <row>
 213         <entry/>
 214         <entry>|</entry>
 215         <entry><link linkend="tac_normalize"><emphasis role="bold">normalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
 216       </row>
 217       <row>
 218         <entry/>
 219         <entry>|</entry>
 220         <entry><link linkend="tac_reduce"><emphasis role="bold">reduce</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
 221       </row>
 222       <row>
 223         <entry/>
 224         <entry>|</entry>
 225         <entry>
 226           <link linkend="tac_reflexivity">
 227             <emphasis role="bold">reflexivity</emphasis>
 228           </link>
 229         </entry>
 230       </row>
 231       <row>
 232         <entry/>
 233         <entry>|</entry>
 234         <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>
 235       </row>
 236       <row>
 237         <entry/>
 238         <entry>|</entry>
 239         <entry><link linkend="tac_rewrite"><emphasis role="bold">rewrite</emphasis></link> [<emphasis role="bold">&lt;</emphasis>|<emphasis role="bold">&gt;</emphasis>] <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
 240       </row>
 241       <row>
 242         <entry/>
 243         <entry>|</entry>
 244         <entry>
 245           <link linkend="tac_right">
 246             <emphasis role="bold">right</emphasis>
 247           </link>
 248         </entry>
 249       </row>
 250       <row>
 251         <entry/>
 252         <entry>|</entry>
 253         <entry>
 254           <link linkend="tac_ring">
 255             <emphasis role="bold">ring</emphasis>
 256           </link>
 257         </entry>
 258       </row>
 259       <row>
 260         <entry/>
 261         <entry>|</entry>
 262         <entry><link linkend="tac_simplify"><emphasis role="bold">simplify</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
 263       </row>
 264       <row>
 265         <entry/>
 266         <entry>|</entry>
 267         <entry>
 268           <link linkend="tac_split">
 269             <emphasis role="bold">split</emphasis>
 270           </link>
 271         </entry>
 272       </row>
 273       <row>
 274         <entry/>
 275         <entry>|</entry>
 276         <entry>
 277           <link linkend="tac_symmetry">
 278             <emphasis role="bold">symmetry</emphasis>
 279           </link>
 280         </entry>
 281       </row>
 282       <row>
 283         <entry/>
 284         <entry>|</entry>
 285         <entry><link linkend="tac_transitivity"><emphasis role="bold">transitivity</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
 286       </row>
 287       <row>
 288         <entry/>
 289         <entry>|</entry>
 290         <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>
 291       </row>
 292       <row>
 293         <entry/>
 294         <entry>|</entry>
 295         <entry><link linkend="tac_whd"><emphasis role="bold">whd</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
 296       </row>
 297     </tbody>
 298   </tgroup>
 299 </table>