(the specification language of <link to="http://matita.cs.unibo.it/">Matita</link>).
The overall validation speed of the "Grundlagen der Analysis"
increases of 34% with respect to version 0.8.1.
- <rlink to="documentation.html#ldJ3a">Documentation (J3a)</rlink>.
+ <rlink to="html/documentation.html#ldJ3a">Documentation (J3a)</rlink>.
[Svn revision: 13035] (<rlink to="download/helena_0.8.2.tar.gz">archived source code</rlink>).
<list><item>
The specification of Landau's "Grundlagen der Analysis"
Supports λδ version 2 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>.
- <rlink to="documentation.html#ldR2a">Documentation (R2a)</rlink>.
+ <rlink to="html/documentation.html#ldR2a">Documentation (R2a)</rlink>.
[Svn revision: 10304] (<rlink to="download/helena_0.8.0.tar.gz">archived source code</rlink>).
<list><item>
A <link to="http://www.jedsoft.org/jed/">Jed mode</link>
<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>).
+ (from Jutting's specification in <link to="http://www.win.tue.nl/automath/">Automath</link>).
</topitem>
<topitem name="access">
- <notice class="alpha" notice="Access:"/>
- <rlink to="static/lddl/">static pages</rlink> (updated <notice class="gamma" notice="2015-01"/>),
+ <notice class="alpha" notice="Access: "/>
+ <rlink to="html/lddl/">html pages</rlink> (updated <notice class="gamma" notice="2019-12"/>),
<rlink to="download/lddl.tar.bz2">data set</rlink> (updated <notice class="gamma" notice="2014-12"/>),
<rlink to="xml/">HELM server URL</rlink> (updated <notice class="gamma" notice="2014-12"/>).
</topitem>
<topitem name="examples">
- <notice class="alpha" notice="Examples:"/>
- <rlink to="static/lddl/Environment/grundlagen_2/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
+ <notice class="alpha" notice="Examples: "/>
+ <rlink to="html/lddl/Environment/grundlagen_2/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
Grundlagen's definition "t234"</rlink>
in λδ version 4.
</topitem>