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

   1 <itemizedlist>
   2   <listitem>
   3     <para><link linkend="tac_absurd"><emphasis role="bold">absurd</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
   4   </listitem>
   5   <listitem>
   6     <para><link linkend="tac_apply"><emphasis role="bold">apply</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
   7   </listitem>
   8   <listitem>
   9     <para>
  10       <link linkend="tac_assumption">
  11         <emphasis role="bold">assumption</emphasis>
  12       </link>
  13     </para>
  14   </listitem>
  15   <listitem>
  16     <para><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>]</para>
  17   </listitem>
  18   <listitem>
  19     <para><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></para>
  20   </listitem>
  21   <listitem>
  22     <para>
  23              <link linkend="tac_clear"><emphasis role="bold">clear</emphasis></link>
  24              <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis><link linkend="grammar.id">id</link></emphasis>…]
  25             </para>
  26   </listitem>
  27   <listitem>
  28     <para><link linkend="tac_clearbody"><emphasis role="bold">clearbody</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis></para>
  29   </listitem>
  30   <listitem>
  31     <para><link linkend="tac_constructor"><emphasis role="bold">constructor</emphasis></link> <emphasis><link linkend="grammar.nat">nat</link></emphasis></para>
  32   </listitem>
  33   <listitem>
  34     <para>
  35       <link linkend="tac_contradiction">
  36         <emphasis role="bold">contradiction</emphasis>
  37       </link>
  38     </para>
  39   </listitem>
  40   <listitem>
  41     <para><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>]</para>
  42   </listitem>
  43   <listitem>
  44     <para>
  45              <link linkend="tac_decompose"><emphasis role="bold">decompose</emphasis></link>
  46              [<emphasis role="bold">(</emphasis>
  47              <emphasis><link linkend="grammar.id">id</link></emphasis>…
  48              <emphasis role="bold">)</emphasis>]
  49              [<emphasis><link linkend="grammar.id">id</link></emphasis>]
  50              [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>…]
  51             </para>
  52   </listitem>
  53   <listitem>
  54     <para>
  55       <link linkend="tac_demodulate">
  56         <emphasis role="bold">demodulate</emphasis>
  57       </link>
  58     </para>
  59   </listitem>
  60   <listitem>
  61     <para><link linkend="tac_discriminate"><emphasis role="bold">discriminate</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
  62   </listitem>
  63   <listitem>
  64     <para><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></para>
  65   </listitem>
  66   <listitem>
  67     <para><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></para>
  68   </listitem>
  69   <listitem>
  70     <para><link linkend="tac_exact"><emphasis role="bold">exact</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
  71   </listitem>
  72   <listitem>
  73     <para>
  74       <link linkend="tac_exists">
  75         <emphasis role="bold">exists</emphasis>
  76       </link>
  77     </para>
  78   </listitem>
  79   <listitem>
  80     <para>
  81       <link linkend="tac_fail">
  82         <emphasis role="bold">fail</emphasis>
  83       </link>
  84     </para>
  85   </listitem>
  86   <listitem>
  87     <para><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></para>
  88   </listitem>
  89   <listitem>
  90     <para>
  91       <link linkend="tac_fourier">
  92         <emphasis role="bold">fourier</emphasis>
  93       </link>
  94     </para>
  95   </listitem>
  96   <listitem>
  97     <para><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>]…]</para>
  98   </listitem>
  99   <listitem>
 100     <para><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>]</para>
 101   </listitem>
 102   <listitem>
 103     <para>
 104       <link linkend="tac_id">
 105         <emphasis role="bold">id</emphasis>
 106       </link>
 107     </para>
 108   </listitem>
 109   <listitem>
 110     <para><link linkend="tac_injection"><emphasis role="bold">injection</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
 111   </listitem>
 112   <listitem>
 113     <para><link linkend="tac_intro"><emphasis role="bold">intro</emphasis></link> [<emphasis><link linkend="grammar.id">id</link></emphasis>]</para>
 114   </listitem>
 115   <listitem>
 116     <para><link linkend="tac_intros"><emphasis role="bold">intros</emphasis></link> <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></para>
 117   </listitem>
 118   <listitem>
 119     <para><link linkend="tac_inversion"><emphasis role="bold">inversion</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
 120   </listitem>
 121   <listitem>
 122     <para>
 123              <link linkend="tac_lapply"><emphasis role="bold">lapply</emphasis></link>
 124              [<emphasis role="bold">linear</emphasis>]
 125              [<emphasis role="bold">depth=</emphasis><emphasis><link linkend="grammar.nat">nat</link></emphasis>]
 126              <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>
 127              [<emphasis role="bold">to</emphasis>
 128               <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>
 129               [<emphasis role="bold">,</emphasis><emphasis><link linkend="grammar.sterm">sterm</link></emphasis>…]
 130              ]
 131              [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]
 132             </para>
 133   </listitem>
 134   <listitem>
 135     <para>
 136       <link linkend="tac_left">
 137         <emphasis role="bold">left</emphasis>
 138       </link>
 139     </para>
 140   </listitem>
 141   <listitem>
 142     <para><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></para>
 143   </listitem>
 144   <listitem>
 145     <para><link linkend="tac_normalize"><emphasis role="bold">normalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
 146   </listitem>
 147   <listitem>
 148     <para><link linkend="tac_paramodulation"><emphasis role="bold">paramodulation</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
 149   </listitem>
 150   <listitem>
 151     <para><link linkend="tac_reduce"><emphasis role="bold">reduce</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
 152   </listitem>
 153   <listitem>
 154     <para>
 155       <link linkend="tac_reflexivity">
 156         <emphasis role="bold">reflexivity</emphasis>
 157       </link>
 158     </para>
 159   </listitem>
 160   <listitem>
 161     <para><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></para>
 162   </listitem>
 163   <listitem>
 164     <para><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></para>
 165   </listitem>
 166   <listitem>
 167     <para>
 168       <link linkend="tac_right">
 169         <emphasis role="bold">right</emphasis>
 170       </link>
 171     </para>
 172   </listitem>
 173   <listitem>
 174     <para>
 175       <link linkend="tac_ring">
 176         <emphasis role="bold">ring</emphasis>
 177       </link>
 178     </para>
 179   </listitem>
 180   <listitem>
 181     <para><link linkend="tac_simplify"><emphasis role="bold">simplify</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
 182   </listitem>
 183   <listitem>
 184     <para>
 185       <link linkend="tac_split">
 186         <emphasis role="bold">split</emphasis>
 187       </link>
 188     </para>
 189   </listitem>
 190   <listitem>
 191     <para>
 192       <link linkend="tac_symmetry">
 193         <emphasis role="bold">symmetry</emphasis>
 194       </link>
 195     </para>
 196   </listitem>
 197   <listitem>
 198     <para><link linkend="tac_transitivity"><emphasis role="bold">transitivity</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
 199   </listitem>
 200   <listitem>
 201     <para><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></para>
 202   </listitem>
 203   <listitem>
 204     <para><link linkend="tac_whd"><emphasis role="bold">whd</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
 205   </listitem>
 206 </itemizedlist>