src/HOL/Analysis/Product_Vector.thy

 end
 
 
 subsection \<open>Product is a real vector space\<close>
 
-instantiation%important prod :: (real_vector, real_vector) real_vector
+instantiation prod :: (real_vector, real_vector) real_vector
 begin
 
 definition scaleR_prod_def:
   "scaleR r A = (scaleR r (fst A), scaleR r (snd A))"
 

 
 subsection \<open>Product is a metric space\<close>
 
 (* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
 
-instantiation%important prod :: (metric_space, metric_space) dist
+instantiation prod :: (metric_space, metric_space) dist
 begin
 
 definition%important dist_prod_def[code del]:
   "dist x y = sqrt ((dist (fst x) (fst y))\<^sup>2 + (dist (snd x) (snd y))\<^sup>2)"
 

   by standard (rule uniformity_prod_def)
 end
 
 declare uniformity_Abort[where 'a="'a :: metric_space \<times> 'b :: metric_space", code]
 
-instantiation%important prod :: (metric_space, metric_space) metric_space
+instantiation prod :: (metric_space, metric_space) metric_space
 begin
 
 lemma dist_Pair_Pair: "dist (a, b) (c, d) = sqrt ((dist a c)\<^sup>2 + (dist b d)\<^sup>2)"
   unfolding dist_prod_def by simp
 

     by (rule convergentI)
 qed
 
 subsection \<open>Product is a normed vector space\<close>
 
-instantiation%important prod :: (real_normed_vector, real_normed_vector) real_normed_vector
+instantiation prod :: (real_normed_vector, real_normed_vector) real_normed_vector
 begin
 
 definition norm_prod_def[code del]:
   "norm x = sqrt ((norm (fst x))\<^sup>2 + (norm (snd x))\<^sup>2)"
 

   by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
 
 
 subsection \<open>Product is an inner product space\<close>
 
-instantiation%important prod :: (real_inner, real_inner) real_inner
+instantiation prod :: (real_inner, real_inner) real_inner
 begin
 
 definition inner_prod_def:
   "inner x y = inner (fst x) (fst y) + inner (snd x) (snd y)"