auto syntax updated

diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index 7647232613daff64928d14d507f7d120439f736e..812c8ed970a2044472bcfd78653955ce29654fb0 100644 (file)
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -184,7 +184,8 @@
         <varlistentry role="tactic.synopsis">
           <term>Synopsis:</term>
           <listitem>
-            <para><emphasis role="bold">auto</emphasis> &autoparams;</para>
+            <para><emphasis role="bold">auto</emphasis> &autoparams;. </para>
+            <para><emphasis role="bold">autobatch</emphasis> &autoparams;</para>
           </listitem>
         </varlistentry>
         <varlistentry>
@@ -195,7 +196,8 @@
              controlled by the optional <command>params</command>.
              Moreover, only lemmas whose type signature is a subset of the
              signature of the current sequent are considered. The signature of
-             a sequent is ...&TODO;</para>
+             a sequent is essentially the set of constats appearing in it.
+           </para>
           </listitem>
         </varlistentry>
         <varlistentry>

diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml
index 15793c63acb9e71b45b1d8065a64a05623f390ec..592e583e4ebfe490c8ae39fae438491216ed8e86 100644 (file)
--- a/helm/software/matita/help/C/sec_terms.xml
+++ b/helm/software/matita/help/C/sec_terms.xml
@@ -737,9 +737,8 @@
        <entry>::=</entry>
         <entry>[&simpleautoparam;]…
                [<emphasis role="bold">by</emphasis>
-                &term; [&term;]…]
+                &term;, [&term;]…]
         </entry>
-        <entry>&TODO;</entry>
        </row>
       </tbody>
      </tgroup>
@@ -752,19 +751,34 @@
        <entry id="grammar.simpleautoparam">&simpleautoparam;</entry>
        <entry>::=</entry>
         <entry><emphasis role="bold">depth=&nat;</emphasis></entry>
-        <entry>&TODO;</entry>
+        <entry>Give a bound to the depth of the search tree</entry>
        </row>
        <row>
         <entry/>
         <entry>|</entry>
         <entry><emphasis role="bold">width=&nat;</emphasis></entry>
-        <entry>&TODO;</entry>
+        <entry>The maximal width of the search tree</entry>
        </row>
        <row>
         <entry/>
         <entry>|</entry>
-        <entry><emphasis role="bold">&TODO;</emphasis></entry>
-        <entry>&TODO;</entry>
+        <entry><emphasis role="bold">library</emphasis></entry>
+        <entry>Search everywhere (not only in included files)</entry>
+       </row>
+       <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><emphasis role="bold">type</emphasis></entry>
+        <entry>Try to close also goals of sort Type, otherwise only goals
+               living in sort Prop are attacked.
+        </entry>
+       </row>
+       <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><emphasis role="bold">paramodulation</emphasis></entry>
+        <entry>Try to close the goal performing unit-equality paramodulation
+        </entry>
        </row>
       </tbody>
      </tgroup>

diff --git a/helm/software/matita/help/C/tactics_quickref.xml b/helm/software/matita/help/C/tactics_quickref.xml
index 331d58dc2902b94461ed3d40d85b2c38d689e663..a7c1ae3bd6039202f44b9e7f27b8e08de02c84ec 100644 (file)
--- a/helm/software/matita/help/C/tactics_quickref.xml
+++ b/helm/software/matita/help/C/tactics_quickref.xml
@@ -29,7 +29,7 @@
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_auto"><emphasis role="bold">auto</emphasis></link> <emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis></entry>
+        <entry><link linkend="tac_auto"><emphasis role="bold">auto</emphasis></link> <emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis>. <emphasis role="bold">autobatch</emphasis> <emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis></entry>
       </row>
       <row>
         <entry/>