- 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 331d58dc2902b94461ed3d40d85b2c38d689e663..c7a789c1a32ed246648eb8577e80afb34aa77862 100644 (file)
--- a/helm/software/matita/help/C/tactics_quickref.xml
+++ b/helm/software/matita/help/C/tactics_quickref.xml
@@ -29,14 +29,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></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 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> [<emphasis role="bold">(</emphasis>[<emphasis><link linkend="grammar.id">id</link></emphasis>]…<emphasis role="bold">)</emphasis>]
            </entry>
       </row>
       <row>
@@ -102,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/>