X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambda_delta%2Fweb%2Fhome%2Fld_basic_2.ldw.xml;h=a542cc19a1838dc5a9cab45f2f6dc565c9821312;hb=afe1661e69d1fdec2a65abe1ea9abdae03874967;hp=080d62ea1a43f22318e376b373a8c9d3f727e107;hpb=2b58d92062882492dd024a1196b6f8b788ffe5c6;p=helm.git
diff --git a/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml b/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml
index 080d62ea1..a542cc19a 100644
--- a/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml
+++ b/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml
@@ -1,14 +1,63 @@
-
- Logical structure of the contribution
- The source files are grouped in planes and components according to the following table.
-
- Physical structure of the contribution
- The source files are grouped in directories, one for each component.
-
-
+ System's Syntax and Behavior
+ This is a summary of the "block structure"
+ of the System's syntactic items and reductions.
+
+
+ * In terms only.
+ ** In terms and local environments only.
+ *** In global environments only.
+ **** Sort level k in terms only.
+
+
+ Summary of the Specification
+ Here is a numerical acount of the specification's contents
+ and its timeline.
+
+
+
+ Context-sensitive subject equivalence
+ for native type assignment.
+
+
+ Context-sensitive subject equivalence
+ for atomic arity assignment.
+
+
+ Context-sensitive strong normalization
+ for simply typed terms.
+
+
+ Support for abstract candidates of reducibility.
+
+
+ Confluence for context-sensitive parallel reduction.
+
+
+ Confluence for context-free parallel reduction.
+
+
+ Specification starts.
+
+
+ Logical Structure of the Specification
+ The source files are grouped in planes and components
+ according to the following table.
+ A notation file covering the whole specification is provided.
+ The notation for the relations or functions introduced in each file
+ is shown in parentheses.
+
+
+
+ Physical Structure of the Specification
+ The source files are grouped in directories,
+ one for each component.
+
+
+