restored the 2 ways of pasting: both "as term" and "as pattern" are available again

[helm.git] / helm / www / matita / matita.shtml
diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml

index 30830764c887d54ad30445ca868b9770ce19ab05..ce58853f7749f710461247d64dcbaacf375a1c53 100644 (file)
--- a/helm/www/matita/matita.shtml
+++ b/helm/www/matita/matita.shtml
@@ -7,6 +7,7 @@
    </head>
    <body>
      <!--#include virtual="menubar.shtml" -->
+    <!--#include virtual="news.shtml" -->
      <div class="main">
  
        <div class="topimage">
@@ -25,10 +26,10 @@
        </span>
        Matita is <strong>traditional</strong>. Its logical foundation is the
        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> encoding of CIC. The interaction
-      paradigm of Matita is familiar, being inspired by CtCoq and
+      mathematical concepts produced by other proof assistants (e.g.
+      <a href="http://coq.inria.fr">Coq</a>) when encoded in an
+      <a href="http://www.w3.org/XML/">XML</a> representation 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>