src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
 changeset 62102 877463945ce9 parent 62101 26c0a70f78a3 child 62397 5ae24f33d343
```     1.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Fri Jan 08 17:40:59 2016 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Fri Jan 08 17:41:04 2016 +0100
1.3 @@ -252,7 +252,7 @@
1.4    fix x :: "'a ^ 'b" show "\<not> open {x}"
1.5    proof
1.6      assume "open {x}"
1.7 -    hence "\<forall>i. open ((\<lambda>x. x \$ i) ` {x})" by (fast intro: open_image_vec_nth)
1.8 +    hence "\<forall>i. open ((\<lambda>x. x \$ i) ` {x})" by (fast intro: open_image_vec_nth)
1.9      hence "\<forall>i. open {x \$ i}" by simp
1.10      thus "False" by (simp add: not_open_singleton)
1.11    qed
1.12 @@ -275,13 +275,15 @@
1.13  begin
1.14
1.15  definition [code del]:
1.16 -  "(uniformity :: (('a, 'b) vec \<times> ('a, 'b) vec) filter) =
1.17 +  "(uniformity :: (('a, 'b) vec \<times> ('a, 'b) vec) filter) =
1.18      (INF e:{0 <..}. principal {(x, y). dist x y < e})"
1.19
1.20 -instance
1.21 +instance
1.22    by standard (rule uniformity_vec_def)
1.23  end
1.24
1.25 +declare uniformity_Abort[where 'a="'a :: metric_space ^ 'b :: finite", code]
1.26 +
1.27  instantiation vec :: (metric_space, finite) metric_space
1.28  begin
1.29
```