near to the final version ...

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 7eeeb83b53641f7f80afccb7b1bbf20b6e5dcaea..d902d1380eab3b0ac781e6332c33f6603528b063 100644 (file)
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -114,10 +114,11 @@
 \section{Introduction}
 \label{sec:intro}
 
-\MATITA{} is the Proof Assistant under development by the \HELM{}
+\MATITA is the Proof Assistant under development by the \HELM{}
 team~\cite{mkm-helm} at the University of Bologna, under the direction of
-Prof.~Asperti. This paper describes the overall architecture of
-the system, focusing on its most distinctive and innovative 
+Prof.~Asperti. \MATITA{} is free software, the source code is available for
+download at \url{http://matita.cs.unibo.it}. This paper describes the overall
+architecture of the system, focusing on its most distinctive and innovative
 features.
 
 \subsection{Historical perspective}
@@ -1577,7 +1578,7 @@ where \texttt{H} is $\beta$-expanded over the second \texttt{n}
 occurrence. 
 
 At this point, since \COQ{} unification algorithm is essentially first-order,
-the application of an elimination principle (of the form $\forall P.\forall
+the application of an elimination principle (a term with type $\forall P.\forall
 x.(H~x)\to (P~x)$) will unify \texttt{x} with \texttt{n} and \texttt{P} with
 \texttt{(fun n0: nat => m + n = n0)}.
 
@@ -1784,7 +1785,7 @@ As a first step in this direction, we will integrate \MATITA{} with a
 revision control system, building on the invalidation and re-generation
 concepts already implemented to grant logical consistency.
 
-Thanks to an increasing dissemination activity, we hope in the medium
+Thanks to an increasing dissemination activity, we hope in the\linebreak medium
 term to attract users to form a critical mass of users to enter in
 direct competition with the (still too few) major actors in the field.
 To this aim, we are also progressing in the development of a core library,