From 4957b21add8195c1e87a947f0de45010d0af683e Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 12 Jul 2006 08:45:32 +0000
Subject: [PATCH] paramodulation is not a stand alone tactic: doc fixed.

---
 matita/help/C/sec_tactics.xml     | 33 -------------------------------
 matita/help/C/tactic_quickref.xml |  5 -----
 2 files changed, 38 deletions(-)

diff --git a/matita/help/C/sec_tactics.xml b/matita/help/C/sec_tactics.xml
index 56037dde5..e9f156723 100644
--- a/matita/help/C/sec_tactics.xml
+++ b/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/matita/help/C/tactic_quickref.xml b/matita/help/C/tactic_quickref.xml
index b41ae79eb..17a031308 100644
--- a/matita/help/C/tactic_quickref.xml
+++ b/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>
-- 
2.39.2