X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Fmatitaprover%2FSystemDescriptionMatita.html;h=ededf325cf5b0cd6c9932920a7119000f8272615;hb=04ae8084273d40d58a391a5a530511c975fbd22d;hp=fbbf4c4bc542f192275be85a669cb8c0536c2041;hpb=fd6372c8268d8dbe17810361bc870c6d8bcd5390;p=helm.git
diff --git a/helm/software/components/binaries/matitaprover/SystemDescriptionMatita.html b/helm/software/components/binaries/matitaprover/SystemDescriptionMatita.html
index fbbf4c4bc..ededf325c 100644
--- a/helm/software/components/binaries/matitaprover/SystemDescriptionMatita.html
+++ b/helm/software/components/binaries/matitaprover/SystemDescriptionMatita.html
@@ -1,5 +1,5 @@
-Matita (prover) 0.5.7
+Matita (prover) 1.0.0
The HELM Team and contributors
University of Bologna, Department of Computer Science
@@ -22,14 +22,14 @@ clauses.
Implementation
Matita is written in Objective Caml, a functional language similar to ML
-developed at INRIA. The automatic prover partecipating to the CASC is
+developed at INRIA. The automatic prover participating to the CASC is
a module of 4000 lines, designed with simplicity and ease of integration in mind.
-It uses the fuctor abstraction mechanism of the OCaml language to achieve
+It uses the functor abstraction mechanism of the OCaml language to achieve
a good degree of reusability (i.e. comparison over terms is an abstract notion,
that can be instantiated with a reduction aware relation for higher order logics
like the Calculus of Inductive Constructions on which Matita is based, or a simpler
-alpha equivalence relation for the TPTP first order lnaguage). Matita is based
-on the Curry-Howard Isomorphims, i.e. proofs are lambda-terms of the CIC calculus.
+alpha equivalence relation for the TPTP first order language). Matita is based
+on the Curry-Howard Isomorphism, i.e. proofs are lambda-terms of the CIC calculus.
The automatic prover is thus able to produce a trace suitable for proof term
reconstruction [HOPR].