X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fweb%2Fhome%2Fimplementation.ldw.xml;h=48ff2c594966c98553b5b4c4493630fa35bd25ca;hb=25577a78cccba09974c91fcbfea770091a413382;hp=1c357b3c1d51cf2ec9bab7947f1e724ecb3bbf78;hpb=37e1b4f314ffae815beca71300688040f8da6939;p=helm.git diff --git a/helm/www/lambdadelta/web/home/implementation.ldw.xml b/helm/www/lambdadelta/web/home/implementation.ldw.xml index 1c357b3c1..48ff2c594 100644 --- a/helm/www/lambdadelta/web/home/implementation.ldw.xml +++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml @@ -14,23 +14,26 @@ The λδ Digital Library is part of HELM and contains resources expressed in λδ. - + + Landau's "Grundlagen der Analysis" (from Jutting's specification in Automath). - - - static pages (updated ), - data set (updated ), - HELM server URL (updated ). - - + + + + static pages (updated ), + data set (updated ), + HELM server URL (updated ). + + + Grundlagen's definition "t234" (in "basic_rg" λδ), Grundlagen's definition "t234" (in "complete_rg" λδ). - + Helena @@ -45,10 +48,12 @@ of the HELM Svn repository. The Svn revisions containing the stable versions of Helena are indicated next. - + + In progress. - - + + + Exploits a subset of "complete_rg" λδ as the intermediate language. Features importation from ".hln" files containing λδ textual syntax. The overall validation speed of the "Grundlagen der Analysis" @@ -58,15 +63,16 @@ A Jed mode for editing ".hln" files (containing λδ textual syntax): helena.sl - (revised ). + (revised ). - + Helena appears in F. Wiedijk's index of computer math systems. - - + + + Supports "basic_rg" λδ with naive implementation of impredicative sort inclusion. Features importation from Automath and exportation to XML. @@ -77,16 +83,16 @@ for editing ".aut" files (containing Automath textual syntax): automath.sl - (revised ). + (revised ). - + Jutting's specification of Landau's "Grundlagen der Analysis" enters λδ Digital Library. - + Jutting's specification of Landau's "Grundlagen der Analysis" is successfully processed, enabling sort inclusion. - +