<listitem><para>Using the "Ctrl+Shift+Unicode code" standard Gnome shortcut. E.g. Ctrl+Shift+3a9 generates "Ω".</para>
</listitem>
<listitem><para>Typing the ligature "\name" where "name"
- is a standard Unicode or LaTeX name for the character. Pressing
- "Alt+L" 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 "\name"
- sequences. E.g. "\Omega" followed by Alt+L generates
- "Ω".</para>
+ is a standard Unicode or LaTeX name for the character or an
+ ASCII art resembling the shape of the character. Pressing
+ "Alt+L" or Space or Enter just after the last character
+ of the name converts
+ the ligature to the Unicode symbol.
+ E.g. "\Delta" followed by Alt+L generates
+ "Δ", while pressing Alt-L after "=>" generates
+ "⇒"</para>
</listitem>
- <listitem><para>Typing one of the following ligatures (and optionally
- converting the ligature to the Unicode character has described before):
- ":=" (which stands for ≝); "->" (which stands for
- "→"); "=>" (which stands for "⇒").</para>
+ <listitem>
+ <para>Typing a symbol and rotating trough its equivalence class
+ with Alt-L. E.g. pressing Alt-L after an "l"
+ generates a "λ", while pressing Alt-L after an
+ "→" once generates "⇉" and pressing
+ Alt-L again generates "⇒".
+ </para>
</listitem>
</itemizedlist>
+ <para>
+ The comprehensive list of symbols names or shortcuts and their equivalence
+ classes is available clicking on the "TeX/UTF-8 table" item
+ of the "View" 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 "_" to generate "⎻"
+ (that is the third choice, after "⎽" and "⎼"),
+ the next time you type Alt-L
+ after "_" you immediately get "⎻".
+ </para>
</sect1>
<sect1 id="cicbrowser">
<title>Browsing and searching</title>