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, the user may also dispose of the source script files,
-while in the case of Coq he may only rely on XML files of
+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.
The current library just comprises about one thousand theorems in
elementary aspects of arithmetics. The most complex result proved