From 54a4872ce3e05e56ca36747df014aa506bd9c71d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 1 Jun 2013 16:42:29 +0000 Subject: [PATCH] update in basic_2 and apps_2 --- helm/www/lambdadelta/BTM.html | 2 +- helm/www/lambdadelta/apps_2.html | 42 +++++++------------ helm/www/lambdadelta/basic_2.html | 10 ++--- .../bin/{xhtbl => }/Makefile.common | 0 helm/www/lambdadelta/bin/xhtbl/Makefile | 2 +- 5 files changed, 22 insertions(+), 34 deletions(-) rename helm/www/lambdadelta/bin/{xhtbl => }/Makefile.common (100%) diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 40a8fa2f3..17efe350b 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -223,6 +223,6 @@

-
Last update: Thu, 16 May 2013 16:37:26 +0200
+
Last update: Sat, 01 Jun 2013 18:41:06 +0200
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index f8b26841b..6e81b110f 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -72,29 +72,29 @@ sizes files - 5 + 4 characters - 5790 + 3928 nodes - 9846 + 3637 propositions theorems - 4 + 2 lemmas 1 total - 5 + 3 concepts declared 3 defined - 10 + 9 total - 13 + 12 @@ -138,29 +138,17 @@ - MLTT1 - - genv_primitive - judgement + functional + reduction and type machine + rtm + rtm_step ( ? ⇨ ? ) - functional - reduction and type machine - rtm - rtm_step ( ? ⇨ ? ) - - - +
- unfold - lift ( ↑[?,?] ? ) - subst ( [?←?] ? ) - - - examples - - + relocation + lift ( ↑[?,?] ? )
@@ -199,6 +187,6 @@

-
Last update: Thu, 16 May 2013 16:37:26 +0200
+
Last update: Sat, 01 Jun 2013 18:41:06 +0200
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 3766523d5..9d7141b4c 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -161,18 +161,18 @@ files 169 characters - 347556 + 348328 nodes - 969490 + 970177 propositions theorems 75 lemmas - 707 + 716 total - 782 + 791 concepts @@ -1004,6 +1004,6 @@

-
Last update: Thu, 16 May 2013 16:37:26 +0200
+
Last update: Sat, 01 Jun 2013 18:41:06 +0200
diff --git a/helm/www/lambdadelta/bin/xhtbl/Makefile.common b/helm/www/lambdadelta/bin/Makefile.common similarity index 100% rename from helm/www/lambdadelta/bin/xhtbl/Makefile.common rename to helm/www/lambdadelta/bin/Makefile.common diff --git a/helm/www/lambdadelta/bin/xhtbl/Makefile b/helm/www/lambdadelta/bin/xhtbl/Makefile index c9bea1a53..e1b330db9 100644 --- a/helm/www/lambdadelta/bin/xhtbl/Makefile +++ b/helm/www/lambdadelta/bin/xhtbl/Makefile @@ -5,7 +5,7 @@ REQUIRES = str YACCFLAGS = -v -include Makefile.common +include ../Makefile.common test: @$(MAKE) --no-print-directory -C ../../ www -- 2.39.2