X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fhelp%2FC%2Ftactics_quickref.xml;h=6da96f66d1fc1852e577a381680d19f3a87d932d;hb=632dfd0a57c9951d0efbd769d6f433c4ef68a314;hp=12e450fdf49da7e988b91a4790a25f50eb9e7043;hpb=94188b0cbaff6340464d90cc13ee246ea7ec3284;p=helm.git

diff --git a/matita/matita/help/C/tactics_quickref.xml b/matita/matita/help/C/tactics_quickref.xml
index 12e450fdf..6da96f66d 100644
--- a/matita/matita/help/C/tactics_quickref.xml
+++ b/matita/matita/help/C/tactics_quickref.xml
@@ -5,115 +5,97 @@
       <row>
         <entry id="grammar.tactic">&tactic;</entry>
         <entry>::=</entry>
-        <entry>
-          <link linkend="tac_#">
-            <emphasis role="bold">#</emphasis>
-          </link>
-          <emphasis>
-            <link linkend="grammar.id">id</link>
-          </emphasis>
-        </entry>
+        <entry><emphasis role="bold">@</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry>
-          <link linkend="tac_##">
-            <emphasis role="bold">##</emphasis>
-          </link>
-        </entry>
+        <entry><link linkend="tac_applyS"><emphasis role="bold">applyS</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis></entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
         <entry>
-          <link linkend="tac_#_">
-            <emphasis role="bold">#_</emphasis>
+          <link linkend="tac_assumption">
+            <emphasis role="bold">assumption</emphasis>
           </link>
         </entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_%"><emphasis role="bold">%</emphasis></link> [<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_*"><emphasis role="bold">*</emphasis></link>
-	     [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</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_-"><emphasis role="bold">-</emphasis></link><emphasis><link linkend="grammar.id">id</link></emphasis>
+	     <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>
 	    </entry>
       </row>
       <row>
         <entry/>
         <entry>|</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>[<emphasis role="bold">&lt;</emphasis>|<link linkend="tac_&gt;"><emphasis role="bold">&gt;</emphasis></link>] <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
+        <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>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_@"><emphasis role="bold">@</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
+        <entry>
+	     <emphasis role="bold">-</emphasis><emphasis><link linkend="grammar.id">id</link></emphasis>
+	    </entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_applyS"><emphasis role="bold">applyS</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.autoparams">auto_params</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_assumption">
-            <emphasis role="bold">assumption</emphasis>
-          </link>
-        </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_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 role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]
 	    </entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <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>
+        <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_cut"><emphasis role="bold">cut</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_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>
+        <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_elim"><emphasis role="bold">elim</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
+        <entry>
+          <emphasis role="bold">#</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></entry>
+        <entry>
+          <emphasis role="bold">#_</emphasis>
+        </entry>
       </row>
       <row>
         <entry/>
@@ -133,12 +115,24 @@
         <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>
+          <emphasis role="bold">##</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>
              [<emphasis role="bold">nodelta</emphasis>]</entry>
       </row>
+      <row>
+        <entry/>
+        <entry>|</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>