src/HOL/Library/Product_Vector.thy
 changeset 37678 0040bafffdef parent 36661 0a5b7b818d65 child 44066 d74182c93f04
```--- a/src/HOL/Library/Product_Vector.thy	Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Library/Product_Vector.thy	Thu Jul 01 16:54:44 2010 +0200
@@ -10,7 +10,7 @@

subsection {* Product is a real vector space *}

-instantiation "*" :: (real_vector, real_vector) real_vector
+instantiation prod :: (real_vector, real_vector) real_vector
begin

definition scaleR_prod_def:
@@ -41,8 +41,7 @@

subsection {* Product is a topological space *}

-instantiation
-  "*" :: (topological_space, topological_space) topological_space
+instantiation prod :: (topological_space, topological_space) topological_space
begin

definition open_prod_def:
@@ -157,8 +156,7 @@

subsection {* Product is a metric space *}

-instantiation
-  "*" :: (metric_space, metric_space) metric_space
+instantiation prod :: (metric_space, metric_space) metric_space
begin

definition dist_prod_def:
@@ -340,7 +338,7 @@

subsection {* Product is a complete metric space *}

-instance "*" :: (complete_space, complete_space) complete_space
+instance prod :: (complete_space, complete_space) complete_space
proof
fix X :: "nat \<Rightarrow> 'a \<times> 'b" assume "Cauchy X"
have 1: "(\<lambda>n. fst (X n)) ----> lim (\<lambda>n. fst (X n))"
@@ -357,8 +355,7 @@

subsection {* Product is a normed vector space *}

-instantiation
-  "*" :: (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:
@@ -397,11 +394,11 @@

end

-instance "*" :: (banach, banach) banach ..
+instance prod :: (banach, banach) banach ..

subsection {* Product is an inner product space *}

-instantiation "*" :: (real_inner, real_inner) real_inner
+instantiation prod :: (real_inner, real_inner) real_inner
begin

definition inner_prod_def:```