From aaa8de04bb771bb61116f1b3f2e6d2e36a326e9b Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 5 Dec 2005 09:25:52 +0000 Subject: [PATCH] Minor changes. --- helm/papers/matita/matita2.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 -- 2.39.5