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