From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 12 Jul 2006 08:45:32 +0000 (+0000)
Subject: paramodulation is not a stand alone tactic: doc fixed.
X-Git-Tag: make_still_working~7091
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=82794854730e383a5e388eeec0f89a77d1d2654c;p=helm.git

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 56037dde5..e9f156723 100644
--- 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 b41ae79eb..17a031308 100644
--- 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>