X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_gettingstarted.xml;h=b067e21ec409f004deffeafc2b4aa001a4a63778;hb=cce6f6dc86e2891f87b2023f35ccc5d73a10a5dd;hp=be9a5f22cb8518c8198c07bb044990fa833fb971;hpb=acf470d78228ce3f6ef8c203531ff2228e033d37;p=helm.git diff --git a/helm/software/matita/help/C/sec_gettingstarted.xml b/helm/software/matita/help/C/sec_gettingstarted.xml index be9a5f22c..b067e21ec 100644 --- a/helm/software/matita/help/C/sec_gettingstarted.xml +++ b/helm/software/matita/help/C/sec_gettingstarted.xml @@ -3,7 +3,7 @@ Getting started - If you are already familiar with the Calculus of (co)Inductive + If you are already familiar with the Calculus of (Co)Inductive Constructions (CIC) and with interactive theorem provers with procedural proof languages (expecially Coq), getting started with Matita is relatively easy. You just need to learn how to type Unicode symbols, how to browse @@ -13,7 +13,7 @@ How to type Unicode symbols Unicode characters can be typed in several ways: - Using the "Shift+Ctrl+Unicode code" standard Gnome shortcut. E.g. Shift+Ctrl+3a9 generates "Ω". + Using the "Ctrl+Shift+Unicode code" standard Gnome shortcut. E.g. Ctrl+Shift+3a9 generates "Ω". Typing the ligature "\name" where "name" is a standard Unicode or LaTeX name for the character. Pressing