X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fhelp%2FC%2Ftactics_quickref.xml;h=6da96f66d1fc1852e577a381680d19f3a87d932d;hb=85fcff9664b400a1cf25f383505638ffe34222b6;hp=c7a789c1a32ed246648eb8577e80afb34aa77862;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/matita/help/C/tactics_quickref.xml b/matita/matita/help/C/tactics_quickref.xml
index c7a789c1a..6da96f66d 100644
--- a/matita/matita/help/C/tactics_quickref.xml
+++ b/matita/matita/help/C/tactics_quickref.xml
@@ -5,12 +5,7 @@
       <row>
         <entry id="grammar.tactic">&tactic;</entry>
         <entry>::=</entry>
-        <entry><link linkend="tac_absurd"><emphasis role="bold">absurd</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry><link linkend="tac_apply"><emphasis role="bold">apply</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
+        <entry><emphasis role="bold">@</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
       </row>
       <row>
         <entry/>
@@ -29,14 +24,14 @@
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_auto"><emphasis role="bold">auto</emphasis></link> <emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis>. <emphasis role="bold">autobatch</emphasis> <emphasis><link linkend="grammar.autoparams">auto_params</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_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><link linkend="grammar.id">id</link></emphasis>]…<emphasis role="bold">)</emphasis>]
+	     <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis>
 	    </entry>
       </row>
       <row>
@@ -48,133 +43,60 @@
         <entry/>
         <entry>|</entry>
         <entry>
-	     <link linkend="tac_clear"><emphasis role="bold">clear</emphasis></link>
-	     <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis><link linkend="grammar.id">id</link></emphasis>…]
+	     <emphasis role="bold">-</emphasis><emphasis><link linkend="grammar.id">id</link></emphasis>
 	    </entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_clearbody"><emphasis role="bold">clearbody</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis></entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry><link linkend="tac_compose"><emphasis role="bold">compose</emphasis></link> [<emphasis><link linkend="grammar.nat">nat</link></emphasis>] <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis role="bold">with</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>] [<emphasis><link linkend="grammar.intros-spec">intros-spec</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_constructor"><emphasis role="bold">constructor</emphasis></link> <emphasis><link linkend="grammar.nat">nat</link></emphasis></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_contradiction">
-            <emphasis role="bold">contradiction</emphasis>
-          </link>
-        </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> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]</entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry>
-	     <link linkend="tac_decompose"><emphasis role="bold">decompose</emphasis></link>
-	     [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</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_demodulate"><emphasis role="bold">demodulate</emphasis></link> <emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis></entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry><link linkend="tac_destruct"><emphasis role="bold">destruct</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</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> [<emphasis role="bold">using</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>] <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <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>
+        <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_exact"><emphasis role="bold">exact</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_exists">
-            <emphasis role="bold">exists</emphasis>
-          </link>
-        </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_fail">
-            <emphasis role="bold">fail</emphasis>
-          </link>
+          <emphasis role="bold">#</emphasis>
+          <emphasis>
+            <link linkend="grammar.id">id</link>
+          </emphasis>
         </entry>
       </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <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>
-      </row>
       <row>
         <entry/>
         <entry>|</entry>
         <entry>
-          <link linkend="tac_fourier">
-            <emphasis role="bold">fourier</emphasis>
-          </link>
+          <emphasis role="bold">#_</emphasis>
         </entry>
       </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <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>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <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>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry>
-          <link linkend="tac_id">
-            <emphasis role="bold">id</emphasis>
-          </link>
-        </entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry><link linkend="tac_intro"><emphasis role="bold">intro</emphasis></link> [<emphasis><link linkend="grammar.id">id</link></emphasis>]</entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry><link linkend="tac_intros"><emphasis role="bold">intros</emphasis></link> <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></entry>
-      </row>
       <row>
         <entry/>
         <entry>|</entry>
@@ -185,118 +107,36 @@
         <entry>|</entry>
         <entry>
 	     <link linkend="tac_lapply"><emphasis role="bold">lapply</emphasis></link> 
-	     [<emphasis role="bold">linear</emphasis>]
-	     [<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 role="bold">,</emphasis><emphasis><link linkend="grammar.sterm">sterm</link></emphasis>…]
-	     ] 
-	     [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]
 	    </entry>
       </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry>
-          <link linkend="tac_left">
-            <emphasis role="bold">left</emphasis>
-          </link>
-        </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><link linkend="tac_normalize"><emphasis role="bold">normalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry>
-          <link linkend="tac_reflexivity">
-            <emphasis role="bold">reflexivity</emphasis>
-          </link>
-        </entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <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>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <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>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry>
-          <link linkend="tac_right">
-            <emphasis role="bold">right</emphasis>
-          </link>
-        </entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry>
-          <link linkend="tac_ring">
-            <emphasis role="bold">ring</emphasis>
-          </link>
-        </entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry><link linkend="tac_simplify"><emphasis role="bold">simplify</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
-      </row>
       <row>
         <entry/>
         <entry>|</entry>
         <entry>
-          <link linkend="tac_split">
-            <emphasis role="bold">split</emphasis>
-          </link>
-        </entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry>
-          <link linkend="tac_subst">
-            <emphasis role="bold">subst</emphasis>
-          </link>
-        </entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry>
-          <link linkend="tac_symmetry">
-            <emphasis role="bold">symmetry</emphasis>
-          </link>
+          <emphasis role="bold">##</emphasis>
         </entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_transitivity"><emphasis role="bold">transitivity</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></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><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>
+        <entry>[<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>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_whd"><emphasis role="bold">whd</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
+        <entry><link linkend="tac_whd"><emphasis role="bold">whd</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> [<emphasis role="bold">nodelta</emphasis>]</entry>
       </row>
     </tbody>
   </tgroup>