wording

diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml
index 3a69a1d72391240af5eebad3ecfb769fd00001e8..ecb47af32b0b0d8b410fabf54635f19f969ab4cb 100644 (file)
--- 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>