Even more tactics documented.

diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index caee727a4ab52835465a31ce12574a0086a42b98..5844ffcea3be4e2525e7b9e34618f58a5aaf77c4 100644 (file)
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -860,22 +860,113 @@ its constructor takes no arguments.</para>
   <sect1 id="tac_letin">
     <title>letin &lt;ident&gt; ≝ &lt;term&gt;</title>
     <titleabbrev>letin</titleabbrev>
-    <para>The tactic <command>letin</command> </para>
+    <para><userinput>letin x ≝ t</userinput></para>
+    <para>
+      <variablelist>
+        <varlistentry>
+          <term>Pre-conditions:</term>
+          <listitem>
+            <para>none.</para>
+          </listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>Action:</term>
+          <listitem>
+            <para>it adds to the context of the current sequent to prove a new
+             definition <command>x ≝ t</command>.</para>
+          </listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>New sequents to prove:</term>
+          <listitem>
+            <para>none.</para>
+          </listitem>
+        </varlistentry>
+      </variablelist>
+    </para>
   </sect1>
   <sect1 id="tac_normalize">
     <title>normalize &lt;pattern&gt;</title>
     <titleabbrev>normalize</titleabbrev>
-    <para>The tactic <command>normalize</command> </para>
+    <para><userinput>normalize patt</userinput></para>
+    <para>
+      <variablelist>
+        <varlistentry>
+          <term>Pre-conditions:</term>
+          <listitem>
+            <para>none.</para>
+          </listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>Action:</term>
+          <listitem>
+            <para>it replaces all the terms matched by <command>patt</command>
+             with their βδιζ-normal form.</para>
+          </listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>New sequents to prove:</term>
+          <listitem>
+            <para>none.</para>
+          </listitem>
+        </varlistentry>
+      </variablelist>
+    </para>
   </sect1>
   <sect1 id="tac_paramodulation">
     <title>paramodulation &lt;pattern&gt;</title>
     <titleabbrev>paramodulation</titleabbrev>
-    <para>The tactic <command>paramodulation</command> </para>
+    <para><userinput>paramodulation patt</userinput></para>
+    <para>
+      <variablelist>
+        <varlistentry>
+          <term>Pre-conditions:</term>
+          <listitem>
+            <para>TODO.</para>
+          </listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>Action:</term>
+          <listitem>
+            <para>TODO.</para>
+          </listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>New sequents to prove:</term>
+          <listitem>
+            <para>TODO.</para>
+          </listitem>
+        </varlistentry>
+      </variablelist>
+    </para>
   </sect1>
   <sect1 id="tac_reduce">
     <title>reduce &lt;pattern&gt;</title>
     <titleabbrev>reduce</titleabbrev>
-    <para>The tactic <command>reduce</command> </para>
+    <para><userinput>reduce patt</userinput></para>
+    <para>
+      <variablelist>
+        <varlistentry>
+          <term>Pre-conditions:</term>
+          <listitem>
+            <para>none.</para>
+          </listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>Action:</term>
+          <listitem>
+            <para>it replaces all the terms matched by <command>patt</command>
+             with their βδιζ-normal form.</para>
+          </listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>New sequents to prove:</term>
+          <listitem>
+            <para>none.</para>
+          </listitem>
+        </varlistentry>
+      </variablelist>
+    </para>
   </sect1>
   <sect1 id="tac_reflexivity">
     <title>reflexivity</title>
@@ -931,7 +1022,30 @@ its constructor takes no arguments.</para>
   <sect1 id="tac_simplify">
     <title>simplify &lt;pattern&gt;</title>
     <titleabbrev>simplify</titleabbrev>
-    <para>The tactic <command>simplify</command> </para>
+    <para><userinput>simplify patt</userinput></para>
+    <para>
+      <variablelist>
+        <varlistentry>
+          <term>Pre-conditions:</term>
+          <listitem>
+            <para>none.</para>
+          </listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>Action:</term>
+          <listitem>
+            <para>it replaces all the terms matched by <command>patt</command>
+             with other convertible terms that are supposed to be simpler.</para>
+          </listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>New sequents to prove:</term>
+          <listitem>
+            <para>none.</para>
+          </listitem>
+        </varlistentry>
+      </variablelist>
+    </para>
   </sect1>
   <sect1 id="tac_split">
     <title>split</title>
@@ -956,7 +1070,30 @@ its constructor takes no arguments.</para>
   <sect1 id="tac_whd">
     <title>whd &lt;pattern&gt;</title>
     <titleabbrev>whd</titleabbrev>
-    <para>The tactic <command>whd</command> </para>
+    <para><userinput>whd patt</userinput></para>
+    <para>
+      <variablelist>
+        <varlistentry>
+          <term>Pre-conditions:</term>
+          <listitem>
+            <para>none.</para>
+          </listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>Action:</term>
+          <listitem>
+            <para>it replaces all the terms matched by <command>patt</command>
+             with their βδιζ-weak-head normal form.</para>
+          </listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>New sequents to prove:</term>
+          <listitem>
+            <para>none.</para>
+          </listitem>
+        </varlistentry>
+      </variablelist>
+    </para>
   </sect1>
 
 </chapter>