1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Jul 01 16:54:42 2010 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Jul 01 16:54:44 2010 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  imports Finite_Cartesian_Product Integration
     1.5  begin
     1.6  
     1.7 -instantiation * :: (real_basis, real_basis) real_basis
     1.8 +instantiation prod :: (real_basis, real_basis) real_basis
     1.9  begin
    1.10  
    1.11  definition "basis i = (if i < DIM('a) then (basis i, 0) else (0, basis (i - DIM('a))))"
    1.12 @@ -131,7 +131,7 @@
    1.13  lemma DIM_prod[simp]: "DIM('a \<times> 'b) = DIM('b::real_basis) + DIM('a::real_basis)"
    1.14    by (rule dimension_eq) (auto simp: basis_prod_def zero_prod_def basis_eq_0_iff)
    1.15  
    1.16 -instance * :: (euclidean_space, euclidean_space) euclidean_space
    1.17 +instance prod :: (euclidean_space, euclidean_space) euclidean_space
    1.18  proof (default, safe)
    1.19    let ?b = "basis :: nat \<Rightarrow> 'a \<times> 'b"
    1.20    fix i j assume "i < DIM('a \<times> 'b)" "j < DIM('a \<times> 'b)"
    1.21 @@ -139,7 +139,7 @@
    1.22      unfolding basis_prod_def by (auto simp: dot_basis)
    1.23  qed
    1.24  
    1.25 -instantiation * :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
    1.26 +instantiation prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
    1.27  begin
    1.28  
    1.29  definition "x \<le> (y::('a\<times>'b)) \<longleftrightarrow> (\<forall>i<DIM('a\<times>'b). x $$ i \<le> y $$ i)"