]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/library/Z/z.ma
.ma inclusions corrected/minimized
[helm.git] / helm / matita / library / Z / z.ma
index 207457a913e4e9c91574cf2e630ea61f3f2feb93..997229763f5fc77f4a62790ffe009bd1d65cd0f0 100644 (file)
@@ -14,8 +14,8 @@
 
 set "baseuri" "cic:/matita/Z/z".
 
+include "datatypes/bool.ma".
 include "nat/nat.ma".
-include "higher_order_defs/functions.ma".
 
 inductive Z : Set \def
   OZ : Z