From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 9 Jun 2006 23:59:27 +0000 (+0000)
Subject: wording
X-Git-Tag: make_still_working~7236
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=eae7632cf7e822dde484d1e630cc58993bfd8d3a;p=helm.git

wording
---

diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml
index 3a69a1d72..ecb47af32 100644
--- a/helm/www/matita/matita.shtml
+++ b/helm/www/matita/matita.shtml
@@ -17,30 +17,30 @@
 	Management</a> tools and techniques. </p>
 
       <p> Matita is <strong>traditional</strong>. Its logical foundation is the
-      Calculus of (Co)Inductive Constructions (CIC), and it can re-use
+      Calculus of (Co)Inductive Constructions (CIC). It can re-use
       mathematical concepts produced by other proof assistants like
       <a href="http://coq.inria.fr">Coq</a> and encoded in an
-      <a href="http://www.w3.org/XML/">XML</a> dialect. The interaction
-      paradigm of Matita is well known, having been inspired by
-      <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>, and its
+      <a href="http://www.w3.org/XML/">XML</a> encoding of CIC. The interaction
+      paradigm of Matita is familiar, being inspired by CtCoq and
+      <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>. Its
       proof language is procedural in the same spirit of LCF. </p>
 
       <p> Matita is <strong>innovative</strong>: </p>
       <ul class="wide">
 
-	<li> its user interface sports high quality bidimensional rendering of
-	proofs and formulae exploiting
-	<a href="http://www.w3.org/Math/">MathML</a> markup, equipped with
-	direct manipulation of the underlying CIC terms; </li>
+	<li> the user interface sports high quality bidimensional rendering of
+	proofs and formulae transformed on-the-fly to
+	<a href="http://www.w3.org/Math/">MathML</a> markup, on which direct
+	manipulation of the underlying CIC terms is still possible; </li>
 
-	<li> its library is distributed: every authored concepts can be
-	published and become part of the Matita library which can be browsed as
-	an hypertext (locally or on the World Wide Web) and searched by means of
-	content-based queries; </li>
+	<li> the knowledge base is distributed: every authored concepts can be
+	published becoming part of the Matita library which can be browsed as
+	an hypertext (locally or on the World Wide Web) and searched by means
+	of content-based queries; </li>
 
 	<li> the tactical language, part of the proof language, has
 	step-by-step semantics, enabling inspection and replaying of deeply
-	structured proof scripts </li>
+	structured proof scripts. </li>
 
       </ul>