src/HOL/Library/Product_Vector.thy
changeset 62102 877463945ce9
parent 62101 26c0a70f78a3
child 62131 1baed43f453e
     1.1 --- a/src/HOL/Library/Product_Vector.thy	Fri Jan 08 17:40:59 2016 +0100
     1.2 +++ b/src/HOL/Library/Product_Vector.thy	Fri Jan 08 17:41:04 2016 +0100
     1.3 @@ -276,13 +276,15 @@
     1.4  begin
     1.5  
     1.6  definition [code del]:
     1.7 -  "(uniformity :: (('a \<times> 'b) \<times> ('a \<times> 'b)) filter) = 
     1.8 +  "(uniformity :: (('a \<times> 'b) \<times> ('a \<times> 'b)) filter) =
     1.9      (INF e:{0 <..}. principal {(x, y). dist x y < e})"
    1.10  
    1.11 -instance 
    1.12 +instance
    1.13    by standard (rule uniformity_prod_def)
    1.14  end
    1.15  
    1.16 +declare uniformity_Abort[where 'a="'a :: metric_space \<times> 'b :: metric_space", code]
    1.17 +
    1.18  instantiation prod :: (metric_space, metric_space) metric_space
    1.19  begin
    1.20  
    1.21 @@ -566,9 +568,9 @@
    1.22  lemma inner_Pair_0: "inner x (0, b) = inner (snd x) b" "inner x (a, 0) = inner (fst x) a"
    1.23      by (cases x, simp)+
    1.24  
    1.25 -lemma 
    1.26 +lemma
    1.27    fixes x :: "'a::real_normed_vector"
    1.28 -  shows norm_Pair1 [simp]: "norm (0,x) = norm x" 
    1.29 +  shows norm_Pair1 [simp]: "norm (0,x) = norm x"
    1.30      and norm_Pair2 [simp]: "norm (x,0) = norm x"
    1.31  by (auto simp: norm_Pair)
    1.32