X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fhelp%2FC%2Fsec_intro.xml;h=19a504c2d96fcfa4222864fd51ee986d5346debb;hb=a04fa03fcea0493e89b725960146cc0c06539583;hp=6c22f46647fe4dad91567fefc8f3af95c5b82634;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git
diff --git a/matita/matita/help/C/sec_intro.xml b/matita/matita/help/C/sec_intro.xml
index 6c22f4664..19a504c2d 100644
--- a/matita/matita/help/C/sec_intro.xml
+++ b/matita/matita/help/C/sec_intro.xml
@@ -26,28 +26,33 @@ of the art. In particular:
An on-line help can be browsed via the Gnome documentation browser.
- Mathematical formulae are rendered in two dimensional notation via MathML and Unicode.
+
+ Mathematical formulae are rendered via Unicode.
+
It allows the use of the typical ambiguous mathematical notation by means of a disambiguating parser.
+
Matita vs Coq
The system shares a common look&feel with the Coq proof assistant
- and its graphical user interface. The two systems have the same logic,
- very close proof languages and similar sets of tactics. Moreover,
- Matita is compatible with the library of Coq.
+ and its graphical user interface. The two systems have variants
+ of the same logic,
+ close proof languages and similar sets of tactics.
From the user point of view the main lacking features
with respect to Coq are:
@@ -68,7 +73,7 @@ of the art. In particular:
several rarely used variants for most of the tactics;
- sections and local variables. To maintain compatibility with the library of Coq, theorems defined inside sections are abstracted by name over the section variables; their instances are explicitly applied to actual arguments by means of explicit named substitutions.
+ sections and local variables.