- lambda_delta: we updated some notation

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / grammar / lenv.ma

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 5aacaf57ccaffe8127fa33a21982074ffe9fb681..ba94738a85847b3a9327fd17d492797210605299 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Basic_2/grammar/term.ma".
+include "basic_2/grammar/term.ma".
 
 (* LOCAL ENVIRONMENTS *******************************************************)
 
@@ -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 *)