"include" command implemented.

[helm.git] / helm / matita / library / Z.ma

diff --git a/helm/matita/library/Z.ma b/helm/matita/library/Z.ma
index 842b952b902ce2b57bf2f901e6331c6bc80a6aed..d0049187a6a2510ef6b463156689491455ccdf50 100644 (file)
--- a/helm/matita/library/Z.ma
+++ b/helm/matita/library/Z.ma
@@ -14,30 +14,7 @@
 
 set "baseuri" "cic:/matita/Z/".
 
-alias id "nat" = "cic:/matita/nat/nat.ind#xpointer(1/1)".
-alias id "O" = "cic:/matita/nat/nat.ind#xpointer(1/1/1)".
-alias id "false" = "cic:/matita/bool/bool.ind#xpointer(1/1/2)".
-alias id "true" = "cic:/matita/bool/bool.ind#xpointer(1/1/1)".
-alias id "Not" = "cic:/matita/logic/Not.con".
-alias id "eq" = "cic:/matita/equality/eq.ind#xpointer(1/1)".
-alias id "if_then_else" = "cic:/matita/bool/if_then_else.con".
-alias id "refl_equal" = "cic:/matita/equality/eq.ind#xpointer(1/1/1)".
-alias id "False" = "cic:/matita/logic/False.ind#xpointer(1/1)".
-alias id "True" = "cic:/matita/logic/True.ind#xpointer(1/1)".
-alias id "sym_eq" = "cic:/matita/equality/sym_eq.con".
-alias id "I" = "cic:/matita/logic/True.ind#xpointer(1/1/1)".
-alias id "S" = "cic:/matita/nat/nat.ind#xpointer(1/1/2)".
-alias id "LT" = "cic:/matita/compare/compare.ind#xpointer(1/1/1)".
-alias id "minus" = "cic:/matita/nat/minus.con".
-alias id "nat_compare" = "cic:/matita/nat/nat_compare.con".
-alias id "plus" = "cic:/matita/nat/plus.con".
-alias id "pred" = "cic:/matita/nat/pred.con".
-alias id "sym_plus" = "cic:/matita/nat/sym_plus.con".
-alias id "nat_compare_invert" = "cic:/matita/nat/nat_compare_invert.con".
-alias id "plus_n_O" = "cic:/matita/nat/plus_n_O.con".
-alias id "plus_n_Sm" = "cic:/matita/nat/plus_n_Sm.con".
-alias id "nat_double_ind" = "cic:/matita/nat/nat_double_ind.con".
-alias id "f_equal" = "cic:/matita/equality/f_equal.con".
+include "nat.ma".
 
 inductive Z : Set \def
   OZ : Z