X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Flibrary.shtml;h=d065b7a9f643a104aac62d96577f14daf08ea5d7;hb=647b419e96770d90a82d7a9e5e8843566a9f93ee;hp=a7c0cf17a588c0173f575a57c8808f3b73eb611e;hpb=7c5a250298d2c872362f235716925ce674c516d7;p=helm.git diff --git a/helm/www/matita/library.shtml b/helm/www/matita/library.shtml index a7c0cf17a..d065b7a9f 100644 --- a/helm/www/matita/library.shtml +++ b/helm/www/matita/library.shtml @@ -12,11 +12,12 @@

Scripts

- The scripts used to generate the knowledge base of - Matita can be browsed on line. + The scripts used to generate the knowledge base of + Matita can be browsed on line.

- The experimental scripts for the next major version of Matita can also be browsed on line. + (Old scripts used in the previous releases of + Matita are still available.)


@@ -41,7 +42,7 @@

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 CerCo Web site + on the CerCo Web site

The Basic Picture

@@ -143,7 +144,7 @@ here.

-

The Formal System λδ (lambda-delta)

+

The Formal System λδ (lambda_delta)

The formal system λδ is a typed λ-calculus that pursues the unification of terms, types, environments and contexts @@ -166,7 +167,7 @@

- See the λδ home page + See the λδ home page for more information.