]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/library/dama/models/nat_uniform.ma
- oCic2NCic and nCic2OCic moved to ng_library
[helm.git] / helm / software / matita / library / dama / models / nat_uniform.ma
index 0b2d4356321fa873044e3db09348b70873535763..691d15dd80a584296fcf8f0029ef445ecf6e6785 100644 (file)
 (*                                                                        *)
 (**************************************************************************)
 
-include "nat_ordered_set.ma".
-include "models/discrete_uniformity.ma".
+include "dama/nat_ordered_set.ma".
+include "dama/models/discrete_uniformity.ma".
 
 definition nat_uniform_space: uniform_space.
 apply (discrete_uniform_space_of_bishop_set ℕ);
 qed.
 
-interpretation "Uniform space N" 'N = nat_uniform_space.
\ No newline at end of file
+interpretation "Uniform space N" 'N = nat_uniform_space.