paramodulation is not a stand alone tactic: doc fixed.

diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index 56037dde56bf7d59f20b4efc6d6b1f848a2b643a..e9f1567239ef53add4626f8705f6f3d37391d415 100644 (file)
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -1232,39 +1232,6 @@ its constructor takes no arguments.</para>
       </variablelist>
     </para>
   </sect1>
-  <sect1 id="tac_paramodulation">
-    <title>paramodulation</title>
-    <titleabbrev>paramodulation</titleabbrev>
-    <para><userinput>paramodulation patt</userinput></para>
-    <para>
-      <variablelist>
-        <varlistentry role="tactic.synopsis">
-          <term>Synopsis:</term>
-          <listitem>
-            <para><emphasis role="bold">paramodulation</emphasis> &pattern;</para>
-          </listitem>
-        </varlistentry>
-        <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</title>
     <titleabbrev>reduce</titleabbrev>

diff --git a/helm/software/matita/help/C/tactic_quickref.xml b/helm/software/matita/help/C/tactic_quickref.xml
index b41ae79eb22189e61e7c2bfb31248a5a9ad7d6e6..17a0313082f2153e76ea9a918fe78a0ff59ec71d 100644 (file)
--- a/helm/software/matita/help/C/tactic_quickref.xml
+++ b/helm/software/matita/help/C/tactic_quickref.xml
@@ -209,11 +209,6 @@
         <entry>|</entry>
         <entry><link linkend="tac_normalize"><emphasis role="bold">normalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
       </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry><link linkend="tac_paramodulation"><emphasis role="bold">paramodulation</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
-      </row>
       <row>
         <entry/>
         <entry>|</entry>