update in groud_2 and models

[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 0205ce8a896f286f0f75154f2eaa4764c9c85ebb..ebd100a26c408c5a242e0b87d221d43838e78692 100644 (file)
--- 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>