]> matita.cs.unibo.it Git - helm.git/commitdiff
Minor changes.
authorAndrea Asperti <andrea.asperti@unibo.it>
Mon, 5 Dec 2005 09:25:52 +0000 (09:25 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Mon, 5 Dec 2005 09:25:52 +0000 (09:25 +0000)
helm/papers/matita/matita2.tex

index b047caea99e904a628b4f7d2d9602c62f1073209..c994cbc127a0f852cc8a66554bb036c4d194fe9f 100644 (file)
@@ -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