From: Andrea Asperti Date: Mon, 5 Dec 2005 09:25:52 +0000 (+0000) Subject: Minor changes. X-Git-Tag: make_still_working~8051 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=aaa8de04bb771bb61116f1b3f2e6d2e36a326e9b;p=helm.git Minor changes. --- diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index b047caea9..c994cbc12 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -1219,8 +1219,8 @@ 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, 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