- new tactic applyP for use in the *P*rocedural script reconstruction

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Base-2 / preamble.ma

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 5bf2f44ef61b2e67060439408e2c106195174026..c2c93f32306e87b10ecdd63f168b7f0c7f72f15e 100644 (file)
--- 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".