X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_tactics.xml;h=cd26700ab703a885027108ae4bd5fa217dea8830;hb=db13adb173da540aefbc2aa2d137cebe8d6a2afe;hp=53a20ac6a78e3c07404d442cb8b7a0de17c7b661;hpb=65317d14f32bc24b3e9ed4ea144833dd8517773a;p=helm.git

diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index 53a20ac6a..cd26700ab 100644
--- 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>