From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 8 Feb 2006 10:55:57 +0000 (+0000)
Subject: Help for the first two tactics.
X-Git-Tag: make_still_working~7598
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=36aa410021caae1783ef25281a01a0580554cc37;p=helm.git

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 e658178ca..82bc536d7 100644
--- 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>