- basics: some support for abstract triangular confluence (which

[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 dc2c643b96873915348ede02dd29f38941044464..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
@@ -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 *)