From ad10eb3697233a2e16b9f32fabe0595c0575f34a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 5 Jan 2009 16:07:15 +0000
Subject: [PATCH] added help on virtuals and UTF-8 equivalence classes

---
 .../matita/help/C/sec_gettingstarted.xml      | 38 ++++++++++++++-----
 1 file changed, 28 insertions(+), 10 deletions(-)

diff --git a/helm/software/matita/help/C/sec_gettingstarted.xml b/helm/software/matita/help/C/sec_gettingstarted.xml
index b0c0a863e..e18f3a067 100644
--- a/helm/software/matita/help/C/sec_gettingstarted.xml
+++ b/helm/software/matita/help/C/sec_gettingstarted.xml
@@ -16,19 +16,37 @@
       <listitem><para>Using the &quot;Ctrl+Shift+Unicode code&quot; standard Gnome shortcut. E.g. Ctrl+Shift+3a9 generates &quot;Ω&quot;.</para>
      </listitem>
      <listitem><para>Typing the ligature &quot;\name&quot; where &quot;name&quot;
-      is a standard Unicode or LaTeX name for the character. Pressing
-      &quot;Alt+L&quot; just after the last character of the name converts
-      the ligature to the Unicode symbol. This operation is
-      not required since Matita understands also the &quot;\name&quot;
-      sequences. E.g. &quot;\Omega&quot; followed by Alt+L generates
-      &quot;Ω&quot;.</para>
+		     is a standard Unicode or LaTeX name for the character or an 
+		     ASCII art resembling the shape of the character. Pressing
+      &quot;Alt+L&quot; or Space or Enter just after the last character 
+      of the name converts
+      the ligature to the Unicode symbol. 
+      E.g. &quot;\Delta&quot; followed by Alt+L generates
+      &quot;Δ&quot;, while pressing Alt-L after &quot;=>&quot; generates
+      &quot;⇒&quot;</para>
      </listitem>
-     <listitem><para>Typing one of the following ligatures (and optionally
-         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;).</para>
+     <listitem>
+	     <para>Typing a symbol and rotating trough its equivalence class
+		   with Alt-L. E.g. pressing Alt-L after an  &quot;l&quot;
+		   generates a &quot;λ&quot;, while pressing Alt-L after an
+		   &quot;→&quot; once generates &quot;⇉&quot; and pressing
+		   Alt-L again generates &quot;⇒&quot;.
+         </para>
      </listitem>
     </itemizedlist>
+    <para>
+    The comprehensive list of symbols names or shortcuts and their equivalence
+    classes is available clicking on the &quot;TeX/UTF-8 table&quot; item
+    of the &quot;View&quot; menu.
+    </para>
+    <para>
+	    There is a memory mechanism related to equivalence classes that
+	    remembers your last choice, making it the default one. For example,
+	    if you use &quot;_&quot; to generate &quot;⎻&quot; 
+	    (that is the third choice, after &quot;⎽&quot; and &quot;⎼&quot;), 
+	    the next time you type Alt-L
+	    after &quot;_&quot; you immediately get &quot;⎻&quot;.
+    </para>
   </sect1>
   <sect1 id="cicbrowser">
    <title>Browsing and searching</title>
-- 
2.39.2