- partial implementation of pattern for case documented

[helm.git] / helm / software / matita / help / C / tactics_quickref.xml

diff --git a/helm/software/matita/help/C/tactics_quickref.xml b/helm/software/matita/help/C/tactics_quickref.xml
index 566d185d019228d1c0ffd7f2ca0320e54afd40c8..c7a789c1a32ed246648eb8577e80afb34aa77862 100644 (file)
--- a/helm/software/matita/help/C/tactics_quickref.xml
+++ b/helm/software/matita/help/C/tactics_quickref.xml
@@ -29,7 +29,15 @@
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_auto"><emphasis role="bold">auto</emphasis></link> <emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis></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>
+      </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>]
+           </entry>
       </row>
       <row>
         <entry/>
@@ -49,6 +57,11 @@
         <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>
+      </row>
       <row>
         <entry/>
         <entry>|</entry>
@@ -73,21 +86,13 @@
         <entry>|</entry>
         <entry>
             <link linkend="tac_decompose"><emphasis role="bold">decompose</emphasis></link>
-            [<emphasis role="bold">(</emphasis>
-            <emphasis><link linkend="grammar.id">id</link></emphasis>…
-            <emphasis role="bold">)</emphasis>]
-            [<emphasis><link linkend="grammar.id">id</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_demodulate">
-            <emphasis role="bold">demodulate</emphasis>
-          </link>
-        </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/>
@@ -97,7 +102,7 @@
       <row>
         <entry/>
         <entry>|</entry>
-        <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>
+        <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/>
@@ -209,11 +214,6 @@
         <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_reduce"><emphasis role="bold">reduce</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
-      </row>
       <row>
         <entry/>
         <entry>|</entry>