The λδ Digital Library is part of <link to="http://helm.cs.unibo.it/">HELM</link>
and contains resources expressed in λδ.
</body>
- <news date="Contents:">
+ <topitem name="contents">
+ <notice class="alpha" notice="Contents:"/>
Landau's "Grundlagen der Analysis"
(from Jutting's specification in <link to="http://www.win.tue.nl/automath/">Automath</link>).
- </news>
- <news date="Access:">
- <rlink to="static/lddl/">static pages</rlink> (updated <date date="2012-10"/>),
- <rlink to="download/lddl.tar.bz2">data set</rlink> (updated <date date="2012-10"/>),
- <rlink to="xml/">HELM server URL</rlink> (updated <date date="2012-10"/>).
- </news>
- <news date="Examples:">
+ </topitem>
+ <topitem name="access">
+ <notice class="alpha" notice="Access:"/>
+ <rlink to="static/lddl/">static pages</rlink> (updated <notice class="beta" notice="2012-10"/>),
+ <rlink to="download/lddl.tar.bz2">data set</rlink> (updated <notice class="beta" notice="2012-10"/>),
+ <rlink to="xml/">HELM server URL</rlink> (updated <notice class="beta" notice="2012-10"/>).
+ </topitem>
+ <topitem name="examples">
+ <notice class="alpha" notice="Examples:"/>
<rlink to="static/lddl/brg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
Grundlagen's definition "t234"</rlink>
(in "basic_rg" λδ),
<rlink to="static/lddl/crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
Grundlagen's definition "t234"</rlink>
(in "complete_rg" λδ).
- </news>
+ </topitem>
<subsection name="helena"><helena-icon/>Helena</subsection>
<body>
of the <link to="http://helm.cs.unibo.it/software/index.html">HELM Svn repository</link>.
The Svn revisions containing the stable versions of Helena are indicated next.
</body>
- <news date="Version 0.8.2.">
+ <topitem name="v2">
+ <notice class="beta" notice="Version 0.8.2."/>
In progress.
- </news>
- <news date="Version 0.8.1 (2010-11).">
+ </topitem>
+ <topitem name="v1">
+ <notice class="beta" notice="Version 0.8.1 (2010-11)."/>
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"
A <link to="http://www.jedsoft.org/jed/">Jed mode</link>
for editing ".hln" files (containing λδ textual syntax):
<rlink to="download/helena.sl">helena.sl</rlink>
- (revised <date date="2010-11"/>).
+ (revised <notice class="alpha" notice="2010-11"/>).
</item><item>
- <date date="2009-12."/>
+ <notice class="beta" notice="2009-12."/>
Helena appears in F. Wiedijk's
<link to="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">
index of computer math systems</link>.
</item></list>
- </news>
- <news date="Version 0.8.0 (2009-09).">
+ </topitem>
+ <topitem name="v0">
+ <notice class="beta" notice="Version 0.8.0 (2009-09)."/>
Supports "basic_rg" λδ with naive implementation of impredicative sort inclusion.
Features importation from <link to="http://www.win.tue.nl/automath/">Automath</link>
and exportation to <link to="http://www.w3.org/XML/">XML</link>.
for editing ".aut" files
(containing <link to="http://www.win.tue.nl/automath/">Automath</link> textual syntax):
<rlink to="download/automath.sl">automath.sl</rlink>
- (revised <date date="2008-07"/>).
+ (revised <notice class="gamma" notice="2008-07"/>).
</item><item>
- <date date="2009-09."/>
+ <notice class="beta" notice="2009-09."/>
Jutting's specification of Landau's "Grundlagen der Analysis"
enters λδ Digital Library.
</item><item>
- <date date="2009-06."/>
+ <notice class="beta" notice="2009-06."/>
Jutting's specification of Landau's "Grundlagen der Analysis"
is successfully processed, enabling sort inclusion.
</item></list>
- </news>
+ </topitem>
<footer/>
</page>
projects / helm.git / blobdiff