From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 30 Jan 2006 16:25:46 +0000 (+0000)
Subject: System section "completed".
X-Git-Tag: make_still_working~7729
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d40dccf9dbf0f1792e0f2cbac3c3b3c8fb0c14cb;p=helm.git

System section "completed".
---

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 9617915f2..9e3739f32 100644
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -221,12 +221,12 @@ that has set a sort of
 standard way to interact with the system. Several procedural proof assistants
 have either adopted or cloned Proof General as their main user interface.
 The authoring interface of \MATITA{} is a clone of the Proof General interface.
+On the contrary, the interface to interact with the library is rather
+innovative and directly inspired by the Web interfaces to our Web servers.
 
-\TODO{item che seguono:}
-\begin{itemize}
- \item sistema indipendente (da \COQ)
- \item compatibilit\`a con sistemi legacy
-\end{itemize}
+\MATITA{} is backward compatible with the XML library of proof objects exported
+from \COQ{}, but, in order to test the actual usability of the system, we are
+also developing a new library of basic results from scratch.
 
 \subsection{Relationship with \COQ{}}