X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_tactics.xml;h=ebd100a26c408c5a242e0b87d221d43838e78692;hb=d3548c16f481b14ce94e64c790bc767c59590050;hp=0205ce8a896f286f0f75154f2eaa4764c9c85ebb;hpb=275a432d33c455d75725d5991e82b62e7d01f68d;p=helm.git

diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index 0205ce8a8..ebd100a26 100644
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -221,7 +221,7 @@
     <title>cases</title>
     <titleabbrev>cases</titleabbrev>
     <para><userinput>
-     cases t hyps
+     cases t pattern hyps
     </userinput></para>
     <para>
       <variablelist>
@@ -230,7 +230,7 @@
           <listitem>
             <para>
 	     <emphasis role="bold">cases</emphasis>
-	     &term; [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]
+	     &term; &pattern; [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]
 	    </para>
           </listitem>
         </varlistentry>
@@ -249,6 +249,12 @@
 	     It proceed by cases on <command>t</command>. The new generated
              hypothesis in each branch are named according to
              <command>hyps</command>.
+             The elimintation predicate is restricted by
+             <command>pattern</command>. In particular, if some hypothesis
+             is listed in <command>pattern</command>, the hypothesis is
+             generalized and cleared before proceeding by cases on
+             <command>t</command>. Currently, we only support patterns of the
+             form <command>H<subscript>1</subscript> … H<subscript>n</subscript> ⊢ %</command>. This limitation will be lifted in the future.
 	    </para>
           </listitem>
         </varlistentry>