X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_tactics.xml;h=130c08e56749cf2f08e9eb607fc3999e19781f83;hb=d7e33f1609c2d990eb52c3e30784a2aa7bdd9b32;hp=c10d2bd337aabc49384f3c7984677369e751fce8;hpb=0fe1347ecafd65a4be26f85595032653f81d1ab3;p=helm.git

diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index c10d2bd33..130c08e56 100644
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -163,27 +163,40 @@
   <sect1 id="tac_clear">
     <title>clear</title>
     <titleabbrev>clear</titleabbrev>
-    <para><userinput>clear H</userinput></para>
+    <para><userinput>
+     clear H<subscript>1</subscript> ... H<subscript>m</subscript>
+    </userinput></para>
     <para>
       <variablelist>
         <varlistentry role="tactic.synopsis">
           <term>Synopsis:</term>
           <listitem>
-            <para><emphasis role="bold">clear</emphasis> &id;</para>
+            <para>
+	     <emphasis role="bold">clear</emphasis>
+	     &id; [&id;…]
+	    </para>
           </listitem>
         </varlistentry>
         <varlistentry>
           <term>Pre-conditions:</term>
           <listitem>
-            <para><command>H</command> must be an hypothesis of the
-             current sequent to prove.</para>
+            <para>
+	     <command>
+	      H<subscript>1</subscript> ... H<subscript>m</subscript>
+	     </command> must be hypotheses of the
+             current sequent to prove.
+	    </para>
           </listitem>
         </varlistentry>
         <varlistentry>
           <term>Action:</term>
           <listitem>
-            <para>It hides the hypothesis <command>H</command> from the
-             current sequent.</para>
+            <para>
+	     It hides the hypotheses 
+             <command>
+	      H<subscript>1</subscript> ... H<subscript>m</subscript>
+             </command> from the current sequent.
+	    </para>
           </listitem>
         </varlistentry>
         <varlistentry>
@@ -382,14 +395,22 @@
     <title>decompose</title>
     <titleabbrev>decompose</titleabbrev>
     <para><userinput>
-     decompose (T<subscript>1</subscript> ... T<subscript>n</subscript>) H hips
+     decompose (T<subscript>1</subscript> ... T<subscript>n</subscript>) 
+     H as H<subscript>1</subscript> ... H<subscript>m</subscript>
     </userinput></para>
     <para>
       <variablelist>
         <varlistentry role="tactic.synopsis">
           <term>Synopsis:</term>
           <listitem>
-            <para><emphasis role="bold">decompose</emphasis> &id; [&id;]… &intros-spec;</para>
+            <para>
+	     <emphasis role="bold">decompose</emphasis>
+	     [<emphasis role="bold">(</emphasis>
+	     &id;…
+	     <emphasis role="bold">)</emphasis>]
+	     [&id;] 
+	     [<emphasis role="bold">as</emphasis> &id;…]
+	    </para>
           </listitem>
         </varlistentry>
         <varlistentry>
@@ -408,9 +429,13 @@
           <term>Action:</term>
           <listitem>
             <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.
+	     Runs <command>
+	      elim H H<subscript>1</subscript> ... H<subscript>m</subscript>
+	     </command>, clears <command>H</command> and tries to run itself
+	     recursively on each new identifier introduced by 
+	     <command>elim</command> in the opened sequents. 
+	     If <command>H</command> is not provided tries this operation on
+	     each premise in the current context.
 	    </para>
           </listitem>
         </varlistentry>
@@ -750,13 +775,13 @@ its constructor takes no arguments.</para>
   <sect1 id="tac_fwd">
     <title>fwd</title>
     <titleabbrev>fwd</titleabbrev>
-    <para><userinput>fwd H</userinput></para>
+    <para><userinput>fwd H as H<subscript>0</subscript> ... H<subscript>n</subscript></userinput></para>
     <para>
       <variablelist>
         <varlistentry role="tactic.synopsis">
           <term>Synopsis:</term>
           <listitem>
-            <para><emphasis role="bold">fwd</emphasis> &id; [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]</para>
+            <para><emphasis role="bold">fwd</emphasis> &id; [<emphasis role="bold">as</emphasis> &id; [&id;]…]</para>
           </listitem>
         </varlistentry>
         <varlistentry>
@@ -775,16 +800,23 @@ its constructor takes no arguments.</para>
 	     This tactic is under development.
              It simplifies the current context by removing
 	     <command>H</command> using the following methods:
-	     forward application of a suitable simplification theorem (chosen
-             automatically) of which the type of <command>H</command> is a
-             premise, decomposition, rewriting. 
+	     forward application (by <command>lapply</command>) of a suitable
+	     simplification theorem, chosen automatically, of which the type
+	     of <command>H</command> is a premise, 
+	     decomposition (by <command>decompose</command>),
+	     rewriting (by <command>rewrite</command>).
+	     <command>H<subscript>0</subscript> ... H<subscript>n</subscript></command>
+	     are passed to the tactics <command>fwd</command> invokes, as
+             names for the premise they introduce.
 	    </para>
           </listitem>
         </varlistentry>
         <varlistentry>
           <term>New sequents to prove:</term>
           <listitem>
-            <para>None.</para>
+            <para>
+	     The ones opened by the tactics <command>fwd</command> invokes.
+	    </para>
           </listitem>
         </varlistentry>
       </variablelist>
@@ -1029,7 +1061,7 @@ its constructor takes no arguments.</para>
     <title>lapply</title>
     <titleabbrev>lapply</titleabbrev>
     <para><userinput>
-     lapply depth=d t 
+     lapply linear depth=d t 
      to t<subscript>1</subscript>, ..., t<subscript>n</subscript> as H
     </userinput></para>
     <para>
@@ -1037,25 +1069,59 @@ its constructor takes no arguments.</para>
         <varlistentry role="tactic.synopsis">
           <term>Synopsis:</term>
           <listitem>
-            <para><emphasis role="bold">lapply</emphasis> [<emphasis role="bold">depth=</emphasis>&nat;] &sterm; [<emphasis role="bold">to</emphasis> &sterm; [&sterm;]…] [<emphasis role="bold">as</emphasis> &id;]</para>
+            <para>
+	     <emphasis role="bold">lapply</emphasis> 
+	     [<emphasis role="bold">linear</emphasis>]
+	     [<emphasis role="bold">depth=</emphasis>&nat;] 
+	     &sterm; 
+	     [<emphasis role="bold">to</emphasis>
+	      &sterm;
+	      [<emphasis role="bold">,</emphasis>&sterm;…]
+	     ] 
+	     [<emphasis role="bold">as</emphasis> &id;]
+	    </para>
           </listitem>
         </varlistentry>
         <varlistentry>
           <term>Pre-conditions:</term>
           <listitem>
-            <para>TODO.</para>
+            <para>
+	     <command>t</command> must have at least <command>d</command>
+	     independent premises and <command>n</command> must not be
+	     greater than <command>d</command>.
+	    </para>
           </listitem>
         </varlistentry>
         <varlistentry>
           <term>Action:</term>
           <listitem>
-            <para>TODO.</para>
+            <para>
+	     Invokes <command>letin H ≝ (t ? ... ?)</command>
+	     with enough <command>?</command>'s to reach the 
+	     <command>d</command>-th independent premise of
+	     <command>t</command>
+	     (<command>d</command> is maximum if unspecified).	     
+	     Then istantiates (by <command>apply</command>) with
+	     t<subscript>1</subscript>, ..., t<subscript>n</subscript>
+	     the <command>?</command>'s corresponding to the first 
+	     <command>n</command> independent premises of
+	     <command>t</command>.
+	     Usually the other <command>?</command>'s preceding the 
+	     <command>n</command>-th independent premise of
+	     <command>t</command> are istantiated as a consequence.
+	     If the <command>linear</command> flag is specified and if 
+	     <command>t, t<subscript>1</subscript>, ..., t<subscript>n</subscript></command>
+	     are (applications of) premises in the current context, they are
+             <command>clear</command>ed. 
+	    </para>
           </listitem>
         </varlistentry>
         <varlistentry>
           <term>New sequents to prove:</term>
           <listitem>
-            <para>TODO.</para>
+            <para>
+	     The ones opened by the tactics <command>lapply</command> invokes.
+	    </para>
           </listitem>
         </varlistentry>
       </variablelist>