\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}.
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.