src/HOL/Analysis/Linear_Algebra.thy
changeset 69597 ff784d5a5bfb
parent 69517 dc20f278e8f3
child 69600 86e8e7347ac0
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Sat Jan 05 17:00:43 2019 +0100
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Sat Jan 05 17:24:33 2019 +0100
     1.3 @@ -35,7 +35,7 @@
     1.4  
     1.5  notation inner (infix "\<bullet>" 70)
     1.6  
     1.7 -text\<open>Equality of vectors in terms of @{term "(\<bullet>)"} products.\<close>
     1.8 +text\<open>Equality of vectors in terms of \<^term>\<open>(\<bullet>)\<close> products.\<close>
     1.9  
    1.10  lemma linear_componentwise:
    1.11    fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_inner"