X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fgrammar%2Flenv.ma;h=ba94738a85847b3a9327fd17d492797210605299;hb=439b6ec33d749ba4e6ae0938e973a85bc23e306e;hp=dc2c643b96873915348ede02dd29f38941044464;hpb=a8c166f1e1baeeae04553058bd179420ada8bbe7;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma
index dc2c643b9..ba94738a8 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma
@@ -36,3 +36,5 @@ interpretation "abbreviation (local environment)"
 
 interpretation "abstraction (local environment)"
    'DxAbst L T = (LPair L Abst T).
+
+(* Basic_1: removed theorems 2: chead_ctail c_tail_ind *)