From 1a009d2d2ca666befca9d3d18fa3cbc462c36963 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 15 Oct 2012 15:26:26 +0000 Subject: [PATCH] - xhtbl: we added the construction + to place several keys in one cell - basic_2_src: corrected and updated to use the operator + --- helm/www/lambda_delta/BTM.html | 4 +- helm/www/lambda_delta/apps_2.html | 4 +- helm/www/lambda_delta/basic_2.html | 6 +- helm/www/lambda_delta/bin/xhtbl/matrix.ml | 12 +-- helm/www/lambda_delta/bin/xhtbl/pass2.ml | 4 +- helm/www/lambda_delta/bin/xhtbl/table.ml | 2 +- helm/www/lambda_delta/bin/xhtbl/textLexer.mll | 1 + .../www/lambda_delta/bin/xhtbl/textParser.mly | 16 +++- .../lambda_delta/bin/xhtbl/textUnparser.ml | 5 +- .../www/lambda_delta/bin/xhtbl/xmlUnparser.ml | 2 +- .../www/lambda_delta/web/home/basic_2_src.tbl | 75 +++++++++++-------- 11 files changed, 76 insertions(+), 55 deletions(-) diff --git a/helm/www/lambda_delta/BTM.html b/helm/www/lambda_delta/BTM.html index f7ad18288..a08104cb2 100644 --- a/helm/www/lambda_delta/BTM.html +++ b/helm/www/lambda_delta/BTM.html @@ -18,8 +18,8 @@
This table shows how the first 45 positive integers are distributed in the four classes.
-
+
classcontents














p
147101316192225283134374043
q
5111517232933354145




s
268141820242632384244


t
39122127303639






-
[Spacer]

[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]

Last update: 2012-10-13T23:29:26+02:00
+
[Spacer]

[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]

Last update: 2012-10-15T17:11:10+02:00
diff --git a/helm/www/lambda_delta/apps_2.html b/helm/www/lambda_delta/apps_2.html index 3000958e8..7c16c7d4b 100644 --- a/helm/www/lambda_delta/apps_2.html +++ b/helm/www/lambda_delta/apps_2.html @@ -51,12 +51,12 @@ The notation for the relations or functions introduced in each file is shown in parentheses (? are placeholders).
-
componentplanefiles
MLTT1
genv_primitivejudgement
functionalreduction and type machinertmrtm_step ( ? ⇨ ? )

unfoldlift ( ↑[?,?] ? )subst ( [?←?] ? )
+
componentplanefiles
MLTT1genv_primitivejudgement
functionalreduction and type machinertmrtm_step ( ? ⇨ ? )

unfoldlift ( ↑[?,?] ? )subst ( [?←?] ? )
Physical Structure of the Specification
The source files are grouped in directories, one for each component.
-
[Spacer]

[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]

Last update: 2012-10-13T23:29:26+02:00
+
[Spacer]

[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]

Last update: 2012-10-15T17:11:10+02:00
diff --git a/helm/www/lambda_delta/basic_2.html b/helm/www/lambda_delta/basic_2.html index 108da399f..13150ff49 100644 --- a/helm/www/lambda_delta/basic_2.html +++ b/helm/www/lambda_delta/basic_2.html @@ -29,7 +29,7 @@
Here is a numerical acount of the specification's contents and its timeline.
-
categoryobjects




sizesfiles199bytes739801

propositionstheorems70lemmas880total950
conceptsdeclared40defined72total112
+
categoryobjects




sizesfiles198bytes733870

propositionstheorems70lemmas879total949
conceptsdeclared40defined72total112