]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/dama/dama/models/nat_uniform.ma
...
[helm.git] / helm / software / matita / contribs / dama / dama / models / nat_uniform.ma
index cffccb59e8367e5386fea9ffc5a45914a2ba91cb..0b2d4356321fa873044e3db09348b70873535763 100644 (file)
@@ -19,4 +19,4 @@ definition nat_uniform_space: uniform_space.
 apply (discrete_uniform_space_of_bishop_set ℕ);
 qed.
 
-interpretation "Uniform space N" 'nat = nat_uniform_space.
\ No newline at end of file
+interpretation "Uniform space N" 'N = nat_uniform_space.
\ No newline at end of file