/me finished reviewing ...

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 3c9bd720b02e2a3c583a21ab6516d808dc5dc198..907573f0c750f7d4abd9ec51f2a1593b780b1eee 100644 (file)
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -1851,18 +1851,19 @@ tactical not atomically.
 \section{Standard library}
 \label{sec:stdlib}
 
-\MATITA{} is \COQ{} compatible, in the sense that every theorem of \COQ{}
-can be read, checked and referenced in further developments. 
-However, in order to test the actual usability of the system, a
-new library of results has been started from scratch. In this case, 
-of course, we wrote (and offer) the source script files, 
-while, in the case of \COQ, \MATITA{} may only rely on XML files of
-\COQ{} objects. 
+\MATITA{} is \COQ{} compatible, in the sense that every theorem of \COQ{} can be
+read, checked and referenced in further developments.  However, in order to test
+the actual usability of the system, a new library of results has been started
+from scratch. In this case, of course, we wrote (and offer) the source scripts,
+while in the case of \COQ{} \MATITA{} may only rely on XML files of \COQ{}
+objects. 
+
 The current library just comprises about one thousand theorems in 
 elementary aspects of arithmetics up to the multiplicative property for 
 Eulers' totient function $\phi$.
+
 The library is organized in five main directories: \texttt{logic} (connectives,
-quantifiers, equality, \ldots), \texttt{datatypes} (basic datatypes and type 
+quantifiers, equality, \ldots), \texttt{datatypes} (basic datatypes and type
 constructors), \texttt{nat} (natural numbers), \texttt{Z} (integers), \texttt{Q}
 (rationals). The most complex development is \texttt{nat}, organized in 25
 scripts, listed in Tab.~\ref{tab:scripts}.
@@ -1886,7 +1887,7 @@ scripts, listed in Tab.~\ref{tab:scripts}.
 
 We do not plan to maintain the library in a centralized way, 
 as most of the systems do. On the contrary we are currently
-developing wiki-technologies to support a collaborative 
+developing wiki-technologies to support collaborative 
 development of the library, encouraging people to expand, 
 modify and elaborate previous contributions.