X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fhelp%2FC%2Fsec_commands.xml;h=a3a6cb8ed01d44b51dcc91da537809878acbf544;hb=cffe307107c93392c8663ec246049c0e55d1ed69;hp=3deaf4b517ae381d6f1bfe0419f22de521c83278;hpb=8f699ab265e380a2d1ab7dba0ee5e8ba5556a84a;p=helm.git

diff --git a/matita/matita/help/C/sec_commands.xml b/matita/matita/help/C/sec_commands.xml
index 3deaf4b51..a3a6cb8ed 100644
--- a/matita/matita/help/C/sec_commands.xml
+++ b/matita/matita/help/C/sec_commands.xml
@@ -326,8 +326,36 @@
             hints (<link linkend="command_alias">aliases</link>).
             On the contrary, theorem and definitions declared in a file can be
            immediately used without including it.</para>
-          <para>The file <command>s</command> is automatically compiled
-	  if it is not compiled yet.
+           <para>The file <command>s</command> is automatically compiled
+	   if it is not compiled yet.
+          </para>
+          <para>
+          If the file <command>s</command> was already included, either
+          directly or recursively, the commands does nothing.
+          </para>
+         </listitem>
+       </varlistentry>
+     </variablelist>
+   </para>
+ </sect1>
+ <sect1 id="command_include_alias">
+   <title>include alias</title>
+   <para><userinput>include alias &quot;s&quot;</userinput></para>
+   <para>
+     <variablelist>
+       <varlistentry>
+         <term>Synopsis:</term>
+         <listitem>
+           <para><emphasis role="bold">include</emphasis> <emphasis role="bold">alias</emphasis> &qstring;</para>
+         </listitem>
+       </varlistentry>
+       <varlistentry>
+         <term>Action:</term>
+         <listitem>
+           <para>Every 
+            <link linkend="interpretation">interpretation</link>
+            declared in the file <command>s</command> is re-declared
+            so to make it the preferred choice for disambiguation.
           </para>
          </listitem>
        </varlistentry>