From: Ferruccio Guidi Date: Fri, 23 May 2014 17:33:16 +0000 (+0000) Subject: update in grond_2 and basic_2 ... X-Git-Tag: make_still_working~921 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0e0e006b0bbb19b39c9a069efb8326a861021bb3;p=helm.git update in grond_2 and basic_2 ... --- diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index ca1e38613..c73cf012e 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -223,6 +223,6 @@

-
Last update: Sun, 11 May 2014 22:18:22 +0200
+
Last update: Fri, 23 May 2014 19:32:07 +0200
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 6a18176d1..d1735136e 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -191,6 +191,6 @@

-
Last update: Sun, 11 May 2014 22:18:22 +0200
+
Last update: Fri, 23 May 2014 19:32:08 +0200
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index c5be39a4f..02e468052 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -58,29 +58,29 @@ sizes files - 344 + 347 characters - 621870 + 629824 nodes - 1716656 + 1745922 propositions theorems - 113 + 114 lemmas - 1254 + 1267 total - 1367 + 1381 concepts declared 53 defined - 79 + 80 total - 132 + 133 @@ -851,13 +851,43 @@
+ + +
+ + lazy pointwise extension of a relation + llpx_sn + llpx_sn_alt llpx_sn_alt2 llpx_sn_tc llpx_sn_leq llpx_sn_ldrop llpx_sn_lpx_sn + +
+ + +
+ + + + +
+ + pointwise union for local environments + llor ( ? ⩖[?] ? ≡ ? ) + +
+ + +
+ + +
+ +
context-sensitive exclusion from free variables cofrees ( ? ⊢ ? ~ϵ 𝐅*[?]⦃?⦄ ) - cofrees_lift + cofrees_alt cofrees_lift
@@ -996,8 +1026,8 @@
global env. slicing - gdrop ( ⇩[?] ? ≡ ? ) - gdrop_gdrop + gget ( ⇩[?] ? ≡ ? ) + gget_gget
@@ -1009,11 +1039,9 @@
- pointwise union for local environments - llor ( ? ⩖[?] ? ≡ ? ) - -
- + contxt-sensitive extended ordinary substitution + cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? ) + cpy_lift cpy_nlift cpy_cpy
@@ -1025,9 +1053,9 @@
- pointwise extension of a relation - llpx_sn - llpx_sn_alt llpx_sn_tc llpx_sn_leq llpx_sn_ldrop llpx_sn_lpx_sn + local env. ref. for extended substitution + lsuby ( ? ⊑×[?,?] ? ) + lsuby_lsuby
@@ -1039,9 +1067,7 @@
- -
- + pointwise extension of a relation lpx_sn lpx_sn_alt lpx_sn_tc lpx_sn_ldrop lpx_sn_lpx_sn @@ -1051,34 +1077,6 @@
- - -
- - contxt-sensitive extended ordinary substitution - cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? ) - cpy_lift cpy_cpy - -
- - -
- - - - -
- - local env. ref. for extended substitution - lsuby ( ? ⊑×[?,?] ? ) - lsuby_lsuby - -
- - -
- -
@@ -1271,6 +1269,6 @@

-
Last update: Sun, 11 May 2014 22:18:22 +0200
+
Last update: Fri, 23 May 2014 19:32:08 +0200
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 34a9cda0f..6477ec5f2 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -56,11 +56,11 @@ sizes files - 29 + 31 characters - 74460 + 75360 nodes - 59601 + 59683 propositions @@ -74,11 +74,11 @@ concepts declared - 40 + 41 defined 25 total - 65 + 66 @@ -234,6 +234,6 @@

-
Last update: Sun, 11 May 2014 22:18:22 +0200
+
Last update: Fri, 23 May 2014 19:32:08 +0200