new documentation for the decompose tactic

diff --git a/helm/software/matita/help/C/Makefile b/helm/software/matita/help/C/Makefile
index a789086dc2de0a66ced99e0bd8b7198173e1f204..fd0e3844f43d8302affa6c65cdd6baf6a0cd1900 100644 (file)
--- a/helm/software/matita/help/C/Makefile
+++ b/helm/software/matita/help/C/Makefile
@@ -8,6 +8,16 @@ TEX_XSL=matita-tex.xsl
 TEX_UNICODE_PATH=$(SRCROOT)/share/texmf/unicode
 TEX_ENV=TEXINPUTS=.:$(TEX_UNICODE_PATH):$(TEX_UNICODE_PATH)/data:
 MAIN=matita.xml
+DEPENDENCES = \
+       legal.xml \
+       sec_install.xml \
+       sec_gettingstarted.xml \
+       sec_intro.xml \
+       sec_terms.xml \
+       sec_tactics.xml \
+       sec_tacticals.xml \
+       sec_commands.xml \
+       sec_usernotation.xml
 
 # one of: "fop", "pdflatex"
 PDF_METHOD=pdflatex
@@ -32,7 +42,7 @@ test:
 
 .PHONY: html
 html: html-stamp
-html-stamp: $(MAIN)
+html-stamp: $(MAIN) $(DEPENDENCES)
        xsltproc $(XHTML_XSL) $<
        touch $@
 

diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml
index cdb5108c88f9dde0134dd75d5a6b17362fc1aaa6..7f259909b70e2f612044b4e42ad265f112561ba8 100644 (file)
--- a/helm/software/matita/help/C/matita.xml
+++ b/helm/software/matita/help/C/matita.xml
@@ -95,7 +95,14 @@
        <affiliation> 
          <address> <email>zacchiro@cs.unibo.it</email> </address> 
        </affiliation> 
-      </author> 
+      </author>
+      <author> 
+       <firstname>Ferruccio</firstname> 
+       <surname>Guidi</surname> 
+       <affiliation> 
+         <address> <email>fguidi@cs.unibo.it</email> </address> 
+       </affiliation> 
+      </author>       
 <!-- This is appropriate place for other contributors: translators,
       maintainers,  etc. Commented out by default.
        <othercredit role="translator">

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>