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=d79c894cab905cd98487192b0e5f1049875b7caa;hp=5bf2f44ef61b2e67060439408e2c106195174026;hpb=1a5e02c5d5048ee6ec7d207b77cd5c2c1bdb3dae;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 5bf2f44ef..c2c93f323 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma
@@ -13,6 +13,4 @@
 (**************************************************************************)
 
 include "Base-1/definitions.ma".
-
-alias symbol "minus" = "Coq's natural minus".
-alias symbol "lt" = "Coq's natural 'less than'".
+include "Legacy-2/theory.ma".