(* *)
(**************************************************************************)
-include "uniform.ma".
-include "bishop_set_rewrite.ma".
+include "dama/uniform.ma".
+include "dama/bishop_set_rewrite.ma".
definition discrete_uniform_space_of_bishop_set:bishop_set → uniform_space.
intro C; apply (mk_uniform_space C);