From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 8 Feb 2006 17:55:19 +0000 (+0000)
Subject: Even more tactics documented.
X-Git-Tag: make_still_working~7578
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5b1432705043c3167e0f97fe25223019ba7b3807;p=helm.git

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 caee727a4..5844ffcea 100644
--- 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>