- new tactic subst removes simple non recursive equalities from the context

[helm.git] / helm / software / matita / help / C / sec_tactics.xml

diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index 53a20ac6a78e3c07404d442cb8b7a0de17c7b661..cd26700ab703a885027108ae4bd5fa217dea8830 100644 (file)
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -1578,6 +1578,46 @@ its constructor takes no arguments.</para>
       </variablelist>
     </para>
   </sect1>
+  
+  <sect1 id="tac_subst">
+    <title>subst</title>
+    <titleabbrev>subst</titleabbrev>
+    <para><userinput>subst</userinput></para>
+    <para>
+      <variablelist>
+        <varlistentry role="tactic.synopsis">
+          <term>Synopsis:</term>
+          <listitem>
+            <para><emphasis role="bold">subst</emphasis></para>
+          </listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>Pre-conditions:</term>
+          <listitem><para>
+           None.
+         </para></listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>Action:</term>
+          <listitem><para>
+           For each premise of the form 
+           <command>H: x = t</command> or <command>H: t = x</command>
+           where <command>x</command> is a local variable and 
+           <command>t</command> does not depend on <command>x</command>,
+           the tactic rewrites <command>H</command> wherever 
+           <command>x</command> appears clearing <command>H</command> and
+           <command>x</command> afterwards.
+         </para></listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>New sequents to prove:</term>
+          <listitem><para>
+           The one opened by the applied tactics.
+          </para></listitem>
+        </varlistentry>
+      </variablelist>
+    </para>
+  </sect1>
   <sect1 id="tac_symmetry">
     <title>symmetry</title>
     <titleabbrev>symmetry</titleabbrev>