matita gtk3: some bugs fixed

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

diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index b9857040779315ff3c9187d44d473c79b24a12ce..ebd100a26c408c5a242e0b87d221d43838e78692 100644 (file)
--- 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>