Help for the first two tactics.

diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index e658178ca339b02a4ca43d0022066e4105d211bd..82bc536d74397e3c3554d196a50dc495be16e731 100644 (file)
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -5,13 +5,63 @@
 
   <sect2 id="tac_absurd">
     <title>absurd &lt;term&gt;</title>
-    <para>The tactic <command>absurd</command> </para>
-<para>
-</para>
+    <para><userinput>absurd P</userinput></para>
+    <para>
+        <varlistentry>
+          <term>Pre-conditions:</term>
+          <listitem>
+            <para><command>P</command> must have type <command>Type</command>.</para>
+          </listitem>
+        </varlistentry>
+      <variablelist>
+        <varlistentry>
+          <term>Action:</term>
+          <listitem>
+            <para>it closes the current goal by eliminating an
+             absurd term.</para>
+          </listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>New sequents to prove:</term>
+          <listitem>
+            <para>it opens two new sequents of conclusion <command>P</command>
+             and <command>¬P</command>.</para>
+          </listitem>
+        </varlistentry>
+      </variablelist>
+    </para>
   </sect2>
   <sect2 id="tac_apply">
     <title>apply &lt;term&gt;</title>
-    <para>The tactic <command>apply</command> </para>
+    <para><userinput>apply t</userinput></para>
+    <para>
+      <variablelist>
+        <varlistentry>
+          <term>Pre-conditions:</term>
+          <listitem>
+            <para><command>t</command> must have type
+             <command>T<subscript>1</subscript> → ... →
+              T<subscript>n</subscript> → G</command>
+             where <command>G</command> can be unified with the conclusion
+             of the current sequent.</para>
+          </listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>Action:</term>
+          <listitem>
+            <para>it closes the current goal by applying <command>t</command>.</para>
+          </listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>New sequents to prove:</term>
+          <listitem>
+            <para>it opens a new goal for each premise 
+             <command>T<subscript>i</subscript></command> that is not
+             instantiated by unification.</para>
+          </listitem>
+        </varlistentry>
+      </variablelist>
+    </para>
   </sect2>
   <sect2 id="tac_assumption">
     <title>assumption</title>