X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fhelp%2FC%2Fsec_intro.xml;h=6c22f46647fe4dad91567fefc8f3af95c5b82634;hb=6f769078a23e6c63706a86a35fdc4e8ba08a5414;hp=a29b4960d1dede420648f00e6eb14720865b2ff5;hpb=63349b091357ba4cf3b9924bd1ffecd543f37252;p=helm.git
diff --git a/matita/help/C/sec_intro.xml b/matita/help/C/sec_intro.xml
index a29b4960d..6c22f4664 100644
--- a/matita/help/C/sec_intro.xml
+++ b/matita/help/C/sec_intro.xml
@@ -5,43 +5,44 @@
Introduction
Features
-
-
- Matita is an interactive theorem prover
+ Matita is an interactive theorem prover
(or proof assistant) with the following characteristics:
-
- It is based on a variant of the Calculus of (co)Inductive
- Constructions (CIC). CIC is also the logic of the Coq proof assistant.
-
- It adopts a procedural proof language, but it has a new
- set of small step tacticals that improve proof structuring and debugging.
-
- It has a stand-alone graphical user interface (GUI) inspired by
- CtCoq/Proof General. The GUI is implemented according to the state
- of the art. In particular:
-
- It is based and fully integrated with Gtk/Gnome.
- An on-line help can be browsed via the Gnome documentation
- browser.
- Mathematical formulae are rendered in two dimensional
- notation via MathML and Unicode.
-
-
- It integrates advanced browsing and searching procedures.
-
- It allows the use of the typical ambiguous mathematical notation
- by means of a disambiguating parser.
-
- It is compatible with the library of Coq (definitions and
- proof objects).
-
+
+ It is based on a variant of the Calculus of (Co)Inductive Constructions (CIC). CIC is also the logic of the Coq proof assistant.
+
+
+ It adopts a procedural proof language, but it has a new set of small step tacticals that improve proof structuring and debugging.
+
+
+ It has a stand-alone graphical user interface (GUI) inspired by
+CtCoq/Proof General. The GUI is implemented according to the state
+of the art. In particular:
+
+
+ It is based and fully integrated with Gtk/Gnome.
+
+
+ An on-line help can be browsed via the Gnome documentation browser.
+
+
+ Mathematical formulae are rendered in two dimensional notation via MathML and Unicode.
+
+
+
+
+ It integrates advanced browsing and searching procedures.
+
+
+ It allows the use of the typical ambiguous mathematical notation by means of a disambiguating parser.
+
+
+ It is compatible with the library of Coq (definitions and proof objects).
+
-
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,
@@ -50,38 +51,46 @@
From the user point of view the main lacking features
with respect to Coq are:
-
- proof extraction;
- an extensible language of tactics;
- automatic implicit arguments;
- several ad-hoc decision procedures;
- 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.
+
+ proof extraction;
+
+
+ an extensible language of tactics;
+
+
+ automatic implicit arguments;
+
+
+ several ad-hoc decision procedures;
+
+
+ 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.
+
-
Still from the user point of view, the main differences with respect
to Coq are:
-
- the language of tacticals that allows execution of partial
- tactical application;
- the unification of the concept of metavariable and existential
- variable;
- terms with subterms that cannot be inferred are always allowed
- as arguments of tactics or other commands;
- ambiguous terms are disambiguated by direct interaction
- with the user;
- theorems and definitions in the library are always accessible
- without needing to require/include them; right now, only notation needs
- to be included to become active, but we plan to remove this limitation.
+
+ the language of tacticals that allows execution of partial tactical application;
+
+
+ the unification of the concept of metavariable and existential variable;
+
+
+ terms with subterms that cannot be inferred are always allowed as arguments of tactics or other commands;
+
+
+ ambiguous terms are disambiguated by direct interaction with the user;
+
+
+ theorems and definitions in the library are always accessible without needing to require/include them; right now, only notation needs to be included to become active, but we plan to remove this limitation.
+
-