- lib: some additions

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / unfold / thin.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma
index 39d4d12c405f292063c49a67cb38ae2c3261b64b..d3eb56c8ef1fac86be3c272e28bdc9971aece7dc 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma
@@ -14,12 +14,12 @@
 
 include "basic_2/unfold/ltpss.ma".
 
-(* LOCAL ENVIRONMENT THINNING ***********************************************)
+(* BASIC LOCAL ENVIRONMENT THINNING *****************************************)
 
 definition thin: nat → nat → relation lenv ≝
                  λd,e,L1,L2. ∃∃L. L1 [d, e] ▶* L & ⇩[d, e] L ≡ L2.
 
-interpretation "thinning (local environment)"
+interpretation "basic thinning (local environment)"
    'TSubst L1 d e L2 = (thin d e L1 L2).
 
 (* Basic properties *********************************************************)