From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 10 Jun 2006 14:44:43 +0000 (+0000)
Subject: new documentation for the decompose tactic
X-Git-Tag: 0.4.95@7852~1348
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f20a7c0ed9571dd5a4c16cbbcfc8474947fcb71c;p=helm.git

new documentation for the decompose tactic
---

diff --git a/matita/help/C/Makefile b/matita/help/C/Makefile
index a789086dc..fd0e3844f 100644
--- a/matita/help/C/Makefile
+++ b/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/matita/help/C/matita.xml b/matita/help/C/matita.xml
index cdb5108c8..7f259909b 100644
--- a/matita/help/C/matita.xml
+++ b/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/matita/help/C/sec_tactics.xml b/matita/help/C/sec_tactics.xml
index 90c7f4975..fc3681074 100644
--- a/matita/help/C/sec_tactics.xml
+++ b/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>