Invocation of paramod

[helm.git] / helm / software / components / binaries / matitaprover / SystemDescriptionMatita.html

diff --git a/helm/software/components/binaries/matitaprover/SystemDescriptionMatita.html b/helm/software/components/binaries/matitaprover/SystemDescriptionMatita.html
index fbbf4c4bc542f192275be85a669cb8c0536c2041..ededf325cf5b0cd6c9932920a7119000f8272615 100644 (file)
--- a/helm/software/components/binaries/matitaprover/SystemDescriptionMatita.html
+++ b/helm/software/components/binaries/matitaprover/SystemDescriptionMatita.html
@@ -1,5 +1,5 @@
 <HR><!------------------------------------------------------------------------>
-<H2>Matita (prover) 0.5.7</H2>
+<H2>Matita (prover) 1.0.0</H2>
 The HELM Team and contributors<BR>
 University of Bologna, Department of Computer Science<BR>
 
@@ -22,14 +22,14 @@ clauses.
 <H3>Implementation</H3>
 
 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].