From: Enrico Tassi Date: Tue, 29 Sep 2009 17:20:47 +0000 (+0000) Subject: ... X-Git-Tag: make_still_working~3415 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=6677f4b55d7d949ab7b8f7133f701bcc1593bbeb;hp=1144eafda5f046c21ceda807f4b5659b3e74147d;p=helm.git ... --- 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.