X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBase-2%2Fpreamble.ma;h=c2c93f32306e87b10ecdd63f168b7f0c7f72f15e;hb=3b8d99d5fdb79a5d979a8e200a4a4307fe362009;hp=114efbd53479edff13a2103421c2283d46a30219;hpb=6ba374cbb94797e58cd997c5b41099dd9f679a57;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma
index 114efbd53..c2c93f323 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma
@@ -14,6 +14,3 @@
 
 include "Base-1/definitions.ma".
 include "Legacy-2/theory.ma".
-
-alias symbol "minus" = "Coq's natural minus".
-alias symbol "lt" = "Coq's natural 'less than'".