@@ -222,6 +222,6 @@

Last update: Fri, 01 Apr 2016 23:30:52 +0200

Last update: Thu, 07 Apr 2016 15:45:51 +0200

diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index a0d1206ed..3ff26013d 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -16,12 +16,12 @@

+ $[\lambda\delta home]$

cic:/matita/lambdadelta/apps_2/ (applications of Î»Î´ version 2)

+ $\lambda\delta rainbow rule$

@@ -73,9 +73,11 @@ version 2 - library + helena + + +
- (static LDDL directory) @@ -93,16 +95,14 @@ version 1 - helena - - -
+ library + (static LDDL directory)

Contents of the Specification

Contents of the Specification $\lambda\delta butterfly$

This specification comprises a collection of checked applications of Î»Î´ version 2. @@ -122,7 +122,7 @@ Helena 0.8. -

Summary of the Specification

Summary of the Specification $\lambda\delta butterfly$

Here is a numerical account of the specification's contents and its timeline. @@ -198,7 +198,7 @@ The MLTT1 component is started. -

Logical Structure of the Specification [spacer]

Logical Structure of the Specification $\lambda\delta butterfly$

This table reports the specification's components and their planes.

@@ -233,7 +233,7 @@

+ $\lambda\delta rainbow rule$

@@ -258,6 +258,6 @@

Last update: Fri, 01 Apr 2016 23:30:52 +0200

Last update: Thu, 07 Apr 2016 15:45:52 +0200

diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html index f4d023145..ba5a602e9 100644 --- a/helm/www/lambdadelta/basic_1.html +++ b/helm/www/lambdadelta/basic_1.html @@ -16,12 +16,12 @@

+ $[\lambda\delta home]$

cic:/BOLOGNA/lambdadelta/basic_1/ (core Î»Î´ version 1)

+ $\lambda\delta rainbow rule$

@@ -73,9 +73,11 @@ version 2 - library + helena + + +
- (static LDDL directory) @@ -93,16 +95,14 @@ version 1 - helena - - -
+ library + (static LDDL directory)

Abstract Syntax and Behavior

Abstract Syntax and Behavior $\lambda\delta butterfly$

This is a summary of available syntactic items and reductions (block structure).

@@ -164,7 +164,7 @@

* In terms only.

Summary of the Specification

Summary of the Specification $\lambda\delta butterfly$

Here is a numerical account of the specification's contents and its timeline. @@ -251,7 +251,7 @@ Specification starts. -

Logical Structure of the Specification

Logical Structure of the Specification $\lambda\delta butterfly$

This table reports the specification's components and their planes.

@@ -798,7 +798,7 @@

+ $\lambda\delta rainbow rule$

@@ -823,6 +823,6 @@

Last update: Fri, 01 Apr 2016 23:30:53 +0200

Last update: Thu, 07 Apr 2016 15:45:52 +0200

diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 5ae7da306..12764cede 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -16,12 +16,12 @@

+ $[\lambda\delta home]$

cic:/matita/lambdadelta/basic_2/ (core Î»Î´ version 2)

+ $\lambda\delta rainbow rule$

@@ -73,9 +73,11 @@ version 2 - library + helena + + +
- (static LDDL directory) @@ -93,11 +95,9 @@ version 1 - helena - - -
+ library + (static LDDL directory) @@ -114,7 +114,7 @@ **** Sort level k in terms only. --> -

Summary of the Specification

Summary of the Specification $\lambda\delta butterfly$

Here is a numerical account of the specification's contents and its timeline. @@ -321,7 +321,7 @@ Î»Î´ version 2 is started. -

Logical Structure of the Specification

Logical Structure of the Specification $\lambda\delta butterfly$

This table reports the specification's components and their planes.

@@ -662,7 +662,7 @@

+ $\lambda\delta rainbow rule$

@@ -687,6 +687,6 @@

Last update: Fri, 01 Apr 2016 23:30:53 +0200

Last update: Thu, 07 Apr 2016 15:45:52 +0200

diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index 29a1e83cb..183e662d6 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -16,12 +16,12 @@

+ $[\lambda\delta home]$

The Formal Systems of the Î»Î´ (\lambda\delta) Family

+ $\lambda\delta rainbow rule$

@@ -73,9 +73,11 @@ version 2 - library + helena + + +
- (static LDDL directory) @@ -93,16 +95,14 @@ version 1 - helena - - -
+ library + (static LDDL directory)

Documentation

Documentation $\lambda\delta butterfly$

BibTeX database of Î»Î´ documentation: @@ -113,7 +113,7 @@ (revised 2015-09).

Î»Î´ version 3 (proposed)

+ $\lambda\delta butterfly$ Î»Î´ version 3 (proposed)

The main source of information is J3a.

@@ -136,7 +136,7 @@

Î»Î´ version 2 (active)

+ $\lambda\delta butterfly$ Î»Î´ version 2 (active)

The main source of information is R2c.

@@ -231,7 +231,7 @@

Î»Î´ version 1 (superseded)

+ $\lambda\delta butterfly$ Î»Î´ version 1 (superseded)

The main source of information is J1a. A summary is available in P1e. @@ -364,7 +364,7 @@

+ $\lambda\delta rainbow rule$

@@ -389,6 +389,6 @@

Last update: Fri, 01 Apr 2016 23:30:52 +0200

Last update: Thu, 07 Apr 2016 15:45:51 +0200

diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html index a29a85f85..a9ecbb29a 100644 --- a/helm/www/lambdadelta/ground_1.html +++ b/helm/www/lambdadelta/ground_1.html @@ -16,12 +16,12 @@

+ $[\lambda\delta home]$

cic:/BOLOGNA/lambdadelta/ground_1/ (background for Î»Î´ version 1)

+ $\lambda\delta rainbow rule$

@@ -73,9 +73,11 @@ version 2 - library + helena + + +
- (static LDDL directory) @@ -93,16 +95,14 @@ version 1 - helena - - -
+ library + (static LDDL directory)

Summary of the Specification

Summary of the Specification $\lambda\delta butterfly$

Here is a numerical account of the specification's contents and its timeline. @@ -177,7 +177,7 @@ Specification starts. -

Logical Structure of the Specification

Logical Structure of the Specification $\lambda\delta butterfly$

This table reports the specification's components and their planes.

@@ -266,7 +266,7 @@

+ $\lambda\delta rainbow rule$

@@ -291,6 +291,6 @@

Last update: Fri, 01 Apr 2016 23:30:53 +0200

Last update: Thu, 07 Apr 2016 15:45:52 +0200

diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index e66ca0d4b..ee6a2cfda 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -16,12 +16,12 @@

+ $[\lambda\delta home]$

cic:/matita/lambdadelta/ground_2/ (background for Î»Î´ version 2)

+ $\lambda\delta rainbow rule$

@@ -73,9 +73,11 @@ version 2 - library + helena + + +
- (static LDDL directory) @@ -93,16 +95,14 @@ version 1 - helena - - -
+ library + (static LDDL directory)

Summary of the Specification

Summary of the Specification $\lambda\delta butterfly$

Here is a numerical account of the specification's contents and its timeline. @@ -189,7 +189,7 @@ Specification starts. -

Logical Structure of the Specification

Logical Structure of the Specification $\lambda\delta butterfly$

This table reports the specification's components and their planes.

@@ -682,7 +682,7 @@

+ $\lambda\delta rainbow rule$

@@ -707,6 +707,6 @@

Last update: Fri, 01 Apr 2016 23:30:52 +0200

Last update: Thu, 07 Apr 2016 15:45:52 +0200

diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index eda6bd935..431b19618 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -16,12 +16,12 @@

+ $[\lambda\delta home]$

The Formal Systems of the Î»Î´ (\lambda\delta) Family

+ $\lambda\delta rainbow rule$

@@ -73,9 +73,11 @@ version 2 - library + helena + + +
- (static LDDL directory) @@ -93,46 +95,26 @@ version 1 - helena - - -
+ library + (static LDDL directory)

Tools

Tools $\lambda\delta butterfly$

Î»Î´ Digital Library (LDDL)

+ +

+ Open Symbolic Notation

- The Î»Î´ Digital Library is part of HELM - and contains resources expressed in the systems of the Î»Î´ family. + Open Symbolic Notation, abbreviated OSN, + is an easy and flexible data-interchange text format + intended for the lightweight representation of + generic abstract syntax trees in the domain of formal systems. + Additional information will appear soon.

- Contents: - Landau's "Grundlagen der Analysis" - (from Jutting's specification in Automath). -

- Access: - static pages (updated 2015-01), - data set (updated 2014-12), - HELM server URL (updated 2014-12). -

- Examples: - - Grundlagen's definition "t234" - in Î»Î´ version 4. -

Helena

@@ -265,8 +247,37 @@ +

+ $[\lambda\delta digital library logo]$ Î»Î´ Digital Library (LDDL)

+ The Î»Î´ Digital Library is part of HELM + and contains resources expressed in the systems of the Î»Î´ family. +

+ Contents: + Landau's "Grundlagen der Analysis" + (from Jutting's specification in Automath). +

+ Access: + static pages (updated 2015-01), + data set (updated 2014-12), + HELM server URL (updated 2014-12). +

+ Examples: + + Grundlagen's definition "t234" + in Î»Î´ version 4. +

+ $\lambda\delta rainbow rule$

@@ -291,6 +302,6 @@

Last update: Fri, 01 Apr 2016 23:30:52 +0200

Last update: Thu, 07 Apr 2016 15:45:51 +0200

diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index d14a8519b..aa7ddd794 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -16,12 +16,12 @@

+ $[\lambda\delta home]$

The Formal Systems of the Î»Î´ (\lambda\delta) Family

+ $\lambda\delta rainbow rule$

@@ -73,9 +73,11 @@ version 2 - library + helena + + +
- (static LDDL directory) @@ -93,16 +95,14 @@ version 1 - helena - - -
+ library + (static LDDL directory)

Foreword

Foreword $\lambda\delta butterfly$

The formal systems of the Î»Î´ (\lambda\delta) family are typed Î»-calculi aiming to support @@ -128,7 +128,7 @@ "Tools" menu â "Internet Options" entry â "General" tab â "Fonts" button.

Citations

Citations $\lambda\delta butterfly$

This is a list of publications citing Î»Î´ documentation. @@ -183,11 +183,11 @@ -

Disclaimer [spacer]

Disclaimer $\lambda\delta butterfly$

- The systens of the Î»Î´ family are not related intentionally to any other system - having (variations of) the symbols Î» and Î´ in its name or syntax. + The systens of the Î»Î´ family are not related intentionally to + any other system having (variations of) the symbols Î» and Î´ in its name or syntax. Examples include (but are not limited to):

@@ -250,8 +250,14 @@ Eindhoven University of Technology, Eindhoven. +

+ Moreover, the systens of the Î»Î´ family are not related intentionally to + the character Lady Lambdadelta, + the Witch of Certainty of the sound novel + Umineko no Naku Koro ni. +

+ $\lambda\delta rainbow rule$

@@ -276,6 +282,6 @@

Last update: Fri, 01 Apr 2016 23:30:52 +0200

Last update: Thu, 07 Apr 2016 15:45:51 +0200

diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index 3971c904e..5ef5c3afc 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -16,12 +16,12 @@

+ $[\lambda\delta home]$

The Formal Systems of the Î»Î´ (\lambda\delta) Family

+ $\lambda\delta rainbow rule$

@@ -73,9 +73,11 @@ version 2 - library + helena + + +
- (static LDDL directory) @@ -93,17 +95,15 @@ version 1 - helena - - -
+ library + (static LDDL directory)

Milestones

Milestones $\lambda\delta butterfly$

@@ -336,7 +336,7 @@

Visibility

Visibility $\lambda\delta butterfly$

@@ -355,7 +355,7 @@

+ $\lambda\delta rainbow rule$

@@ -380,6 +380,6 @@

Last update: Fri, 01 Apr 2016 23:30:52 +0200

Last update: Thu, 07 Apr 2016 15:45:51 +0200

diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index 41de39477..b89a7b0f0 100644 --- a/helm/www/lambdadelta/specification.html +++ b/helm/www/lambdadelta/specification.html @@ -16,12 +16,12 @@

+ $[\lambda\delta home]$

The Formal Systems of the Î»Î´ (\lambda\delta) Family

+ $\lambda\delta rainbow rule$

@@ -73,9 +73,11 @@ version 2 - library + helena + + +
- (static LDDL directory) @@ -93,16 +95,14 @@ version 1 - helena - - -
+ library + (static LDDL directory)

Computer-checked formal specifications

Computer-checked formal specifications $\lambda\delta butterfly$

The systems of the Î»Î´ family are developed as machine-checked digital specifications, @@ -245,14 +245,14 @@

Î»Î´ version 3 (proposed)

+ $\lambda\delta butterfly$ Î»Î´ version 3 (proposed)

The formal specification of Î»Î´ version 3 is forthcoming.

Î»Î´ version 2 (active)

+ $\lambda\delta butterfly$ Î»Î´ version 2 (active)

The formal specification of Î»Î´ version 2 is available in the following formats: @@ -284,7 +284,7 @@

Î»Î´ version 1 (superseded)

+ $\lambda\delta butterfly$ Î»Î´ version 1 (superseded)

The formal specification of Î»Î´ version 1 is available in the following formats: @@ -357,7 +357,7 @@ Core.

+ $\lambda\delta rainbow rule$

@@ -382,6 +382,6 @@

Last update: Fri, 01 Apr 2016 23:30:52 +0200

Last update: Thu, 07 Apr 2016 15:45:51 +0200