]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/www/matita/library.shtml
0.5.9 released
[helm.git] / helm / www / matita / library.shtml
index a7c0cf17a588c0173f575a57c8808f3b73eb611e..d065b7a9f643a104aac62d96577f14daf08ea5d7 100644 (file)
 
       <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>
          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
       </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>