From 26778a467329055d706f9b8d9d6869f17186e453 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 26 May 2006 15:39:29 +0000
Subject: [PATCH 1/1] Documentation fixed.

---
 .../matita/help/C/sec_gettingstarted.xml      |  3 +--
 helm/software/matita/help/C/sec_terms.xml     | 22 +++++++++++++++----
 2 files changed, 19 insertions(+), 6 deletions(-)

diff --git a/helm/software/matita/help/C/sec_gettingstarted.xml b/helm/software/matita/help/C/sec_gettingstarted.xml
index f7d435e70..c1feb6d92 100644
--- a/helm/software/matita/help/C/sec_gettingstarted.xml
+++ b/helm/software/matita/help/C/sec_gettingstarted.xml
@@ -26,8 +26,7 @@
      </listitem>
      <listitem>Typing one of the following ligatures (and opzionally converting
       the ligature to the Unicode character has described before):
-      &quot;:=&quot; (which stands for ≝); &quot;->&quot; (which stands for &quot;→&quot;);
-      &quot;->&quot; (which stands for &quot;⇒&quot;).
+      &quot;:=&quot; (which stands for ≝); &quot;->&quot; (which stands for &quot;→&quot;); &quot;=>&quot; (which stands for &quot;⇒&quot;).
      </listitem>
     </itemizedlist>
   </sect1>
diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml
index 45459572b..dd2af7f5f 100644
--- a/helm/software/matita/help/C/sec_terms.xml
+++ b/helm/software/matita/help/C/sec_terms.xml
@@ -158,8 +158,8 @@
       <entry/>
       <entry>|</entry>
       <entry>&id;[<emphasis role="bold">\subst[</emphasis>
-       &id;<emphasis role="bold">≝</emphasis>&term;
-       [<emphasis role="bold">;</emphasis>&id;<emphasis role="bold">≝</emphasis>&term;]…
+       &id;<emphasis role="bold">≔</emphasis>&term;
+       [<emphasis role="bold">;</emphasis>&id;<emphasis role="bold">≔</emphasis>&term;]…
        <emphasis role="bold">]</emphasis>]
       </entry>
       <entry>identifier with optional explicit named substitution</entry>
@@ -249,16 +249,30 @@
       <entry id="args">&args;</entry>
       <entry>::=</entry>
       <entry>
-       [<emphasis role="bold">(</emphasis>]<emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;][<emphasis role="bold">)</emphasis>]
+       <emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]
       </entry>
       <entry>ignored argument</entry>
      </row>
      <row>
       <entry/>
       <entry>|</entry>
-      <entry>[<emphasis role="bold">(</emphasis>]&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;][<emphasis role="bold">)</emphasis>]</entry>
+      <entry>
+       <emphasis role="bold">(</emphasis><emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis>
+      </entry>
+      <entry>ignored argument</entry>
+     </row>
+     <row>
+      <entry/>
+      <entry>|</entry>
+      <entry>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]</entry>
       <entry></entry>
      </row>
+     <row>
+      <entry/>
+      <entry>|</entry>
+      <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis></entry>
+      <entry/>
+     </row>
     </tbody>
    </tgroup>
   </table>
-- 
2.39.2