</body>
<body>
The life cycle of a specification consists of four periods.
- <notice class="alpha" notice="Alpha:"/>
+ <notice class="alpha" text="Alpha:"/>
the definitions are designed and the major propositions are proved,
then the calculus is announced with a presentation.
- <notice class="beta" notice="Beta:"/>
+ <notice class="beta" text="Beta:"/>
major changes and additions may occur before the calculus is released on paper.
- <notice class="gamma" notice="Gamma:"/>
+ <notice class="gamma" text="Gamma:"/>
subsequent improvements occur until the specification is completed or superseded,
while major changes and additions are announced and reported on paper.
- <notice class="delta" notice="Delta:"/>
+ <notice class="delta" text="Delta:"/>
after its conclusion, the specification is modified just for maintenance.
</body>
<table name="versions"/>
<body>
Informational pages on the specifications are provided.
</body>
- <topitem>
- <notice class="alpha" notice="Notice on displayed numerical acounts:"/>
+ <topitem name="notice1">
+ <notice class="alpha" text="Notice on displayed numerical acounts:"/>
nodes are counted according to the "intrinsic complexity measure"
[F. Guidi: "Procedural Representation of CIC Proof Terms"
Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78].
</topitem>
- <topitem>
- <notice class="alpha" notice="Notice on displayed logical structures:"/>
+ <topitem name="notice2">
+ <notice class="alpha" text="Notice on displayed logical structures:"/>
from the logical standpoint, the source scripts are grouped in "planes"
and these are grouped in "components";
the notation for the relations or functions
<topitem name="source2">
<body>
<rlink to="download/lambdadelta_2A1.tar.gz">lambdadelta_2A1 for Matita 0.99.2</rlink>
- (revised <notice class="gamma" notice="2014-10"/>).
+ (revised <notice class="gamma" text="2014-10"/>).
Source scripts.
<rlink to="documentation.html#ldR2c">Documentation (R2c)</rlink>.
</body>
The scripts are grouped in directories, first by part, then by component.
</body>
<body>
- <notice class="alpha" notice="Notice:"/>
+ <notice class="alpha" text="Notice:"/>
the scripts are checked by the latest version of Matita from
<link to="http://matita.cs.unibo.it/download.shtml">HELM Subversion repository</link>
at path <trunk/matita/>.
<topitem name="source1">
<body>
<rlink to="download/lambdadelta_1.tar.gz">lambdadelta_1 for Coq 7.3.1</rlink>
- (revised <notice class="delta" notice="2015-09"/>).
+ (revised <notice class="delta" text="2015-09"/>).
Source scripts.
<rlink to="documentation.html#ldJ1a">Documentation (J1a)</rlink>.
<list><item>
- <notice class="delta" notice="2015 January 15."/>
+ <notice class="delta" text="2015 January 15."/>
17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg".
</item></list>
</body>
<topitem name="static1">
<rlink to="static/matita/lambdadelta/">lambdadelta_1 for Matita 0.5</rlink>
- (revised <notice class="delta" notice="2011-09"/>).
+ (revised <notice class="delta" text="2011-09"/>).
Static HTML pages generated by the <link to="http://helm.cs.unibo.it/">HELM</link> rendering engine.
<list><item>
<rlink to="static/matita/lambdadelta/basic_1/pr3/pr3/pr3_confluence.con.html">
<topitem name="dynamic1">
<link to="http://mowgli.cs.unibo.it:58080/apply?keys=RT&xmluri=http://helm.cs.unibo.it/helm//html/folder/index.html&prop.media-type=text/html&param.thmedia-type=text/html&param.thkeys=T1%2CT2%2CL%2CE&param.embedkeys=d_c%2CTC1%2CHC2%2CL&param.thencoding=UTF-8&prop.encoding=UTF-8&prop.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&param.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&param.encoding=UTF-8&param.media-type=text/html&param.keys=d_c%2CC1%2CHC2%2CL&profile=default&param.profile=default&param.CICURI=theory:/matita/lambdadelta/">
lambdadelta_1 for Matita 0.5</link>
- (revised <notice class="delta" notice="2011-09"/>).
+ (revised <notice class="delta" text="2011-09"/>).
<link to="http://helm.cs.unibo.it/">HELM</link> directory.
- <notice class="alpha" notice="Notice: the HELM rendering engine is offline."/>
+ <notice class="alpha" text="Notice: the HELM rendering engine is offline."/>
</topitem>
<body>
projects / helm.git / blobdiff