More documentation committed.

diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml
index 7b3b3d30c00dc43c6151ea7cf1bc744d13d77bc1..cdb5108c88f9dde0134dd75d5a6b17362fc1aaa6 100644 (file)
--- a/helm/software/matita/help/C/matita.xml
+++ b/helm/software/matita/help/C/matita.xml
@@ -33,6 +33,9 @@
   <!ENTITY args "<emphasis><link linkend='args'>args</link></emphasis>">
   <!ENTITY args2 "<emphasis><link linkend='args2'>args2</link></emphasis>">
   <!ENTITY sterm "<emphasis><link linkend='sterm'>sterm</link></emphasis>">
+  <!ENTITY intros-spec "<emphasis><link linkend='intros-spec'>intros-spec</link></emphasis>">
+  <!ENTITY pattern "<emphasis><link linkend='pattern'>pattern</link></emphasis>">
+  <!ENTITY reduction-kind "<emphasis><link linkend='reduction-kind'>reduction-kind</link></emphasis>">
 ]>
 
 <?yelp:chunk-depth 3?>

diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index 01d9ea63e32cb82e1cd27895f849e9cc08a0b21c..90c7f49757699601a1620d5608d7c22f43b8a03e 100644 (file)
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -188,7 +188,7 @@
     </para>
   </sect1>
   <sect1 id="tac_change">
-    <title><emphasis role="bold">change</emphasis> &lt;pattern&gt; <emphasis role="bold">with</emphasis> &sterm;</title>
+    <title><emphasis role="bold">change</emphasis> &pattern; <emphasis role="bold">with</emphasis> &sterm;</title>
     <titleabbrev>change</titleabbrev>
     <para><userinput>change patt with t</userinput></para>
     <para>
@@ -312,7 +312,7 @@
     </para>
   </sect1>
   <sect1 id="tac_decompose">
-    <title><emphasis role="bold">decompose</emphasis> &id; [&id;]… [&lt;intros_spec&gt;]</title>
+    <title><emphasis role="bold">decompose</emphasis> &id; [&id;]… &intros-spec;</title>
     <titleabbrev>decompose</titleabbrev>
     <para><userinput>decompose ???</userinput></para>
     <para>
@@ -338,6 +338,33 @@
       </variablelist>
     </para>
   </sect1>
+  <sect1 id="tac_demodulation">
+    <title><emphasis role="bold">demodulation</emphasis> &pattern;</title>
+    <titleabbrev>demodulation</titleabbrev>
+    <para><userinput>demodulation patt</userinput></para>
+    <para>
+      <variablelist>
+        <varlistentry>
+          <term>Pre-conditions:</term>
+          <listitem>
+            <para>None.</para>
+          </listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>Action:</term>
+          <listitem>
+            <para>&TODO;</para>
+          </listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>New sequents to prove:</term>
+          <listitem>
+            <para>None.</para>
+          </listitem>
+        </varlistentry>
+      </variablelist>
+    </para>
+  </sect1>
   <sect1 id="tac_discriminate">
     <title><emphasis role="bold">discriminate</emphasis> &sterm;</title>
     <titleabbrev>discriminate</titleabbrev>
@@ -368,7 +395,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_elim">
-    <title><emphasis role="bold">elim</emphasis> &sterm; [<emphasis role="bold">using</emphasis> &sterm;] [&lt;intros_spec&gt;]</title>
+    <title><emphasis role="bold">elim</emphasis> &sterm; [<emphasis role="bold">using</emphasis> &sterm;] &intros-spec;</title>
     <titleabbrev>elim</titleabbrev>
     <para><userinput>elim t using th hyps</userinput></para>
     <para>
@@ -405,7 +432,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_elimType">
-    <title><emphasis role="bold">elimType</emphasis> &sterm; [<emphasis role="bold">using</emphasis> &sterm;] [&lt;intros_spec&gt;]</title>
+    <title><emphasis role="bold">elimType</emphasis> &sterm; [<emphasis role="bold">using</emphasis> &sterm;] &intros-spec;</title>
     <titleabbrev>elimType</titleabbrev>
     <para><userinput>elimType T using th hyps</userinput></para>
     <para>
@@ -518,7 +545,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_fold">
-    <title><emphasis role="bold">fold</emphasis> &lt;reduction_kind&gt; &sterm; &lt;pattern&gt;</title>
+    <title><emphasis role="bold">fold</emphasis> &reduction-kind; &sterm; &pattern;</title>
     <titleabbrev>fold</titleabbrev>
     <para><userinput>fold red t patt</userinput></para>
     <para>
@@ -580,7 +607,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_fwd">
-    <title><emphasis role="bold">fwd</emphasis> &id; [&lt;ident list&gt;]</title>
+    <title><emphasis role="bold">fwd</emphasis> &id; [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]</title>
     <titleabbrev>fwd</titleabbrev>
     <para><userinput>fwd ...TODO</userinput></para>
     <para>
@@ -607,7 +634,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_generalize">
-    <title><emphasis role="bold">generalize</emphasis> &lt;pattern&gt; [<emphasis role="bold">as</emphasis> &id;]</title>
+    <title><emphasis role="bold">generalize</emphasis> &pattern; [<emphasis role="bold">as</emphasis> &id;]</title>
     <titleabbrev>generalize</titleabbrev>
     <para><userinput>generalize patt as H</userinput></para>
     <para>
@@ -734,7 +761,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_intros">
-    <title><emphasis role="bold">intros</emphasis> &lt;intros_spec&gt;</title>
+    <title><emphasis role="bold">intros</emphasis> &intros-spec;</title>
     <titleabbrev>intros</titleabbrev>
     <para><userinput>intros hyps</userinput></para>
     <para>
@@ -806,7 +833,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_lapply">
-    <title><emphasis role="bold">lapply</emphasis> [<emphasis role="bold">depth=</emphasis>&nat;] &sterm; [<emphasis role="bold">to</emphasis> &lt;term list&gt;] [<emphasis role="bold">using</emphasis> &id;]</title>
+    <title><emphasis role="bold">lapply</emphasis> [<emphasis role="bold">depth=</emphasis>&nat;] &sterm; [<emphasis role="bold">to</emphasis> &sterm; [&sterm;]…] [<emphasis role="bold">using</emphasis> &id;]</title>
     <titleabbrev>lapply</titleabbrev>
     <para><userinput>lapply ???</userinput></para>
     <para>
@@ -892,7 +919,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_normalize">
-    <title><emphasis role="bold">normalize</emphasis> &lt;pattern&gt;</title>
+    <title><emphasis role="bold">normalize</emphasis> &pattern;</title>
     <titleabbrev>normalize</titleabbrev>
     <para><userinput>normalize patt</userinput></para>
     <para>
@@ -920,7 +947,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_paramodulation">
-    <title><emphasis role="bold">paramodulation</emphasis> &lt;pattern&gt;</title>
+    <title><emphasis role="bold">paramodulation</emphasis> &pattern;</title>
     <titleabbrev>paramodulation</titleabbrev>
     <para><userinput>paramodulation patt</userinput></para>
     <para>
@@ -947,7 +974,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_reduce">
-    <title><emphasis role="bold">reduce</emphasis> &lt;pattern&gt;</title>
+    <title><emphasis role="bold">reduce</emphasis> &pattern;</title>
     <titleabbrev>reduce</titleabbrev>
     <para><userinput>reduce patt</userinput></para>
     <para>
@@ -1004,7 +1031,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_replace">
-    <title><emphasis role="bold">replace</emphasis> &lt;pattern&gt; <emphasis role="bold">with</emphasis> &sterm;</title>
+    <title><emphasis role="bold">replace</emphasis> &pattern; <emphasis role="bold">with</emphasis> &sterm;</title>
     <titleabbrev>change</titleabbrev>
     <para><userinput>change patt with t</userinput></para>
     <para>
@@ -1036,7 +1063,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_rewrite">
-    <title><emphasis role="bold">rewrite</emphasis> [<emphasis role="bold">&lt;</emphasis>|<emphasis role="bold">&gt;</emphasis>] &sterm; &lt;pattern&gt;</title>
+    <title><emphasis role="bold">rewrite</emphasis> [<emphasis role="bold">&lt;</emphasis>|<emphasis role="bold">&gt;</emphasis>] &sterm; &pattern;</title>
     <titleabbrev>rewrite</titleabbrev>
     <para><userinput>rewrite dir p patt</userinput></para>
     <para>
@@ -1133,7 +1160,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_simplify">
-    <title><emphasis role="bold">simplify</emphasis> &lt;pattern&gt;</title>
+    <title><emphasis role="bold">simplify</emphasis> &pattern;</title>
     <titleabbrev>simplify</titleabbrev>
     <para><userinput>simplify patt</userinput></para>
     <para>
@@ -1250,7 +1277,7 @@ the current sequent to prove.</para>
     </para>
   </sect1>
   <sect1 id="tac_unfold">
-    <title><emphasis role="bold">unfold</emphasis> [&sterm;] &lt;pattern&gt;</title>
+    <title><emphasis role="bold">unfold</emphasis> [&sterm;] &pattern;</title>
     <titleabbrev>unfold</titleabbrev>
     <para><userinput>unfold t patt</userinput></para>
     <para>
@@ -1282,7 +1309,7 @@ the current sequent to prove.</para>
     </para>
   </sect1>
   <sect1 id="tac_whd">
-    <title><emphasis role="bold">whd</emphasis> &lt;pattern&gt;</title>
+    <title><emphasis role="bold">whd</emphasis> &pattern;</title>
     <titleabbrev>whd</titleabbrev>
     <para><userinput>whd patt</userinput></para>
     <para>

diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml
index c50e590b0636ecbdc9132e17da5d2383372e2d26..d2594c718ba2c35d753c3e4c9c6a1edb1ab04039 100644 (file)
--- a/helm/software/matita/help/C/sec_terms.xml
+++ b/helm/software/matita/help/C/sec_terms.xml
@@ -478,5 +478,95 @@
    </sect2>
   </sect1>
 
+  <sect1 id="tacticargs">
+   <title>Tactic arguments</title>
+   <para>This section documents the syntax of some recurring arguments for
+    tactics.</para>
+
+    <sect2 id="introsspec">
+    <title>intros-spec</title>
+    <table frame="all" rowsep="0" colsep="0">
+      <title>intros-spec</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+       <entry id="intros-spec">&intros-spec;</entry>
+       <entry>::=</entry>
+        <entry>[&nat;] [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]</entry>
+       </row>
+      </tbody>
+     </tgroup>
+    </table>
+        <para>The natural number is the number of new hypotheses to be introduced. The list of identifiers gives the name for the first hypotheses.</para>
+    </sect2>
+
+    <sect2 id="pattern">
+    <title>pattern</title>
+    <table frame="all" rowsep="0" colsep="0">
+      <title>pattern</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+       <entry id="pattern">&pattern;</entry>
+       <entry>::=</entry>
+        <entry>&TODO;</entry>
+       </row>
+      </tbody>
+     </tgroup>
+    </table>
+        <para>&TODO;</para>
+    </sect2>
+
+    <sect2 id="reduction-kind">
+    <title>reduction-kind</title>
+    <para>Reduction kinds are normalization functions that transform a term
+     to a convertible but simpler one. Each reduction kind can be used both
+     as a tactic argument and as a stand-alone tactic.</para>
+    <table frame="all" rowsep="0" colsep="0">
+      <title>reduction-kind</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+       <entry id="reduction-kind">&reduction-kind;</entry>
+       <entry>::=</entry>
+        <entry><emphasis role="bold">demodulate</emphasis></entry>
+       </row>
+       <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><emphasis role="bold">normalize</emphasis></entry>
+        <entry>Computes the βδιζ-normal form</entry>
+       </row>
+       <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><emphasis role="bold">reduce</emphasis></entry>
+        <entry>Computes the βδιζ-normal form</entry>
+       </row>
+       <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><emphasis role="bold">simplify</emphasis></entry>
+        <entry>Computes a form supposed to be simpler</entry>
+       </row>
+       <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><emphasis role="bold">unfold</emphasis> [&sterm;]</entry>
+        <entry>δ-reduces the constant or variable specified, or that
+         in head position if none is specified</entry>
+       </row>
+       <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><emphasis role="bold">whd</emphasis></entry>
+        <entry>Computes the βδιζ-weak-head normal form</entry>
+       </row>
+      </tbody>
+     </tgroup>
+    </table>
+    </sect2>
+  </sect1>
+
 </chapter>