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
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