From: Claudio Sacerdoti Coen Date: Wed, 12 Jul 2006 08:45:32 +0000 (+0000) Subject: paramodulation is not a stand alone tactic: doc fixed. X-Git-Tag: 0.4.95@7852~1225 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4957b21add8195c1e87a947f0de45010d0af683e;p=helm.git paramodulation is not a stand alone tactic: doc fixed. --- 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. - - paramodulation - paramodulation - paramodulation patt - - - - Synopsis: - - paramodulation &pattern; - - - - Pre-conditions: - - TODO. - - - - Action: - - TODO. - - - - New sequents to prove: - - TODO. - - - - - reduce reduce 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 @@ | normalize pattern - - - | - paramodulation pattern - |