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