src/HOL/Library/Euclidean_Space.thy
changeset 31275 1ba01cdd9a9a
parent 31118 541d43bee678
child 31285 0a3f9ee4117c
     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Wed May 27 21:46:50 2009 -0700
     1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Thu May 28 09:46:43 2009 +0200
     1.3 @@ -109,10 +109,10 @@
     1.4  
     1.5  text{* Also the scalar-vector multiplication. *}
     1.6  
     1.7 -definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'n" (infixr "*s" 75)
     1.8 +definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'n" (infixl "*s" 70)
     1.9    where "c *s x = (\<chi> i. c * (x$i))"
    1.10  
    1.11 -text{* Constant Vectors *}
    1.12 +text{* Constant Vectors *} 
    1.13  
    1.14  definition "vec x = (\<chi> i. x)"
    1.15