new documentation for the decompose tactic

[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 90c7f49757699601a1620d5608d7c22f43b8a03e..fc3681074429c8f29b7d90b975937df1628332ec 100644 (file)
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -314,25 +314,39 @@
   <sect1 id="tac_decompose">
     <title><emphasis role="bold">decompose</emphasis> &id; [&id;]… &intros-spec;</title>
     <titleabbrev>decompose</titleabbrev>
-    <para><userinput>decompose ???</userinput></para>
+    <para><userinput>
+     decompose (T<subscript>1</subscript> ... T<subscript>n</subscript>) H hips
+    </userinput></para>
     <para>
       <variablelist>
         <varlistentry>
           <term>Pre-conditions:</term>
           <listitem>
-            <para>TODO.</para>
+            <para> 
+            <command>H</command> must inhabit one inductive type among  
+            <command>
+             T<subscript>1</subscript> ... T<subscript>n</subscript>
+            </command>
+            and the types of a predefined list.
+           </para>
           </listitem>
         </varlistentry>
         <varlistentry>
           <term>Action:</term>
           <listitem>
-            <para>TODO.</para>
+            <para>
+            Runs <command>elim H hyps</command>, clears H and tries to run
+             itself recursively on each new identifier introduced by 
+            <command>elim</command> in the opened sequents.
+           </para>
           </listitem>
         </varlistentry>
         <varlistentry>
           <term>New sequents to prove:</term>
           <listitem>
-            <para>TODO.</para>
+            <para>
+            The ones generated by all the <command>elim</command> tactics run.
+           </para>
           </listitem>
         </varlistentry>
       </variablelist>
@@ -835,7 +849,10 @@ its constructor takes no arguments.</para>
   <sect1 id="tac_lapply">
     <title><emphasis role="bold">lapply</emphasis> [<emphasis role="bold">depth=</emphasis>&nat;] &sterm; [<emphasis role="bold">to</emphasis> &sterm; [&sterm;]…] [<emphasis role="bold">using</emphasis> &id;]</title>
     <titleabbrev>lapply</titleabbrev>
-    <para><userinput>lapply ???</userinput></para>
+    <para><userinput>
+     lapply depth=d t 
+     to t<subscript>1</subscript>, ..., t<subscript>n</subscript> using H
+    </userinput></para>
     <para>
       <variablelist>
         <varlistentry>