X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Flibrary.shtml;h=d065b7a9f643a104aac62d96577f14daf08ea5d7;hb=d2545ffd201b1aa49887313791386add78fa8603;hp=9874142c96d59067111f30163cc1e4ca4dfddfb8;hpb=c2a490a6bc12986720b2c84d6916854c6931e08d;p=helm.git

diff --git a/helm/www/matita/library.shtml b/helm/www/matita/library.shtml
index 9874142c9..d065b7a9f 100644
--- a/helm/www/matita/library.shtml
+++ b/helm/www/matita/library.shtml
@@ -12,11 +12,12 @@
 
       <h2>Scripts<a name="scripts"></a></h2>
       <p>
-      The <a href="library/">scripts</a> used to generate the knowledge base of
-      Matita can be <a href="library/">browsed on line</a>.
+      The <a href="nlibrary/">scripts</a> used to generate the knowledge base of
+      Matita can be <a href="nlibrary/">browsed on line</a>.
       </p>
       <p>
-      The experimental <a href="nlibrary/">scripts</a> for the next major version of Matita can also be <a href="nlibrary/">browsed on line</a>.
+      (Old <a href="library/">scripts</a> used in the previous releases of
+      Matita are <a href="library/">still available</a>.)
       </p>
 
       <br/>
@@ -41,7 +42,7 @@
        <p>The CerCo project is a FET Open IST project funded by the EU
           community in the 7th Framework Programme. More informations on the
           project and the code of the Matita formalization can be found
-          on the <a href="cerco.cs.unibo.it">CerCo Web site</a>
+          on the <a href="http://cerco.cs.unibo.it">CerCo Web site</a>
        </p>
 
       <h2>The Basic Picture<a name="sambin"></a></h2>
@@ -52,7 +53,7 @@
       <p>The formalization has been the result of a three years long
        collaboration between mathematicians from the University of Padova
        and computer scientists from the University of
-       Bologna, sponsored by the University of Padova. In particular,
+       Bologna, funded by the University of Padova. In particular,
        the groups that collaborated are headed respectively by Prof. Sambin
        in Padua (formal topology and constructive type theory)
        and by Prof. Asperti in Bologna (constructive type theory and interactive
@@ -71,21 +72,23 @@
            adjunction between topological spaces and locales</li>
       </ul>
       <p>
-      All the results are presented constructively and in the predicative
-      fragment of Matita, without any reference to choice axioms.
+      All the results are presented constructively and in the predicative 
+      fragment of Matita based on the minimalist type theory
+      by Maietti and Sambin, where choice axioms are not valid.
       </p>
-      In order to reason conformtably on the previous concrete categories and
+      In order to reason comfortably on the previous concrete categories and
       functors, we also present algebraic versions of all the introduced
       notions, as well as categorical embedding of the concrete categories in
-      the algebraized ones. In particular we formalized:
+      the algebrized ones. In particular we formalized:
       </p>
       <ul>
-       <li>the large category of Overlap Algebras, that extend locales with an
+       <li>the large category of Overlap Algebras, that extends locales with an
            axiomatized (= algebraized) overlap binary predicate. The
            concrete overlap predicate states positively 
            (i.e. without using negation) the existence (in the intuitionistic
            sense) of a point in the intersection of two sets.
-           The natural morphism over Overlap Algebras are functions for the
+           Morphisms of Overlap Algebras algebrize concrete relations between
+           sets by means of four functions that capture the
            existential and universal pre and post images of a relation.
            </li>
        <li>the large category of O-Basic Pairs, that algebraize Basic
@@ -141,7 +144,7 @@
          here</a>.
       </p>
 
-      <h2>The Formal System &lambda;&delta; (lambda-delta)<a name="lambda-delta"></a></h2>
+      <h2>The Formal System &lambda;&delta; (lambda_delta)<a name="lambda_delta"></a></h2>
       
       <p>The formal system &lambda;&delta; is a typed &lambda;-calculus that
          pursues the unification of terms, types, environments and contexts
@@ -164,7 +167,7 @@
       </p>
       
       <p>
-       See the <a href="http://helm.cs.unibo.it/lambda-delta/">&lambda;&delta; home page</a>
+       See the <a href="http://lambda-delta.info/">&lambda;&delta; home page</a>
        for more information.
       </p>