(* *)
(**************************************************************************)
-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.