From d40dccf9dbf0f1792e0f2cbac3c3b3c8fb0c14cb Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 30 Jan 2006 16:25:46 +0000 Subject: [PATCH] System section "completed". --- helm/papers/matita/matita2.tex | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) 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{}} -- 2.39.2