X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_tactics.xml;h=ebd100a26c408c5a242e0b87d221d43838e78692;hb=refs%2Fheads%2Fmatita-lablgtk3;hp=b9857040779315ff3c9187d44d473c79b24a12ce;hpb=393187c5f5a6e71d467ab04b65f3a935701724fb;p=helm.git

diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index b98570407..ebd100a26 100644
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -61,7 +61,7 @@
           <term>Pre-conditions:</term>
           <listitem>
             <para><command>t</command> must have type
-             <command>T<subscript>1</subscript> → ... →
+             <command>T<subscript>1</subscript> → … →
               T<subscript>n</subscript> → G</command>
              where <command>G</command> can be unified with the conclusion
              of the current sequent.</para>
@@ -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>