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
```