From 6677f4b55d7d949ab7b8f7133f701bcc1593bbeb Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 29 Sep 2009 17:20:47 +0000 Subject: [PATCH] ... --- helm/software/matita/nlibrary/topology/igft.ma | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma index c8317f37e..81aefd555 100644 --- a/helm/software/matita/nlibrary/topology/igft.ma +++ b/helm/software/matita/nlibrary/topology/igft.ma @@ -21,7 +21,7 @@ to make the formalization (at least the definitions and proved statements) readable to the author of the paper. Orienteering ------------ +------------ The graphical interface of Matita is composed of three windows: the script window, on the left, is where you type; the sequent @@ -60,13 +60,13 @@ implements two unusual input facilities: to mean double or single arrows. Here we recall some of these "shortcuts": - - ∀ `\Forall` - - λ `\lambda` - - ≝ `\def` or `:=` - - → `to` or `->` + - ∀ can be typed with `\Forall` + - λ can be typed with `\lambda` + - ≝ can be typed with `\def` or `:=` + - → can be typed with `to` or `->` -- some symbols have variants, like the ≤ relation and ≲, ≼, ≰, ⋠. - The use can cycle between variants typing one them and then +- some symbols have variants, like the ≤ relation and ≼, ≰, ⋠. + The user can cycle between variants typing one of them and then pressing ALT-L. Note that also letters do have variants, for example W has Ω, 𝕎 and 𝐖, L has Λ, 𝕃, and 𝐋, F has Φ, … Variants are listed in the aforementioned TeX/UTF-8 table. -- 2.39.2