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