src/HOL/Analysis/Linear_Algebra.thy
changeset 69674 fc252acb7100
parent 69619 3f7d8e05e0f2
child 69675 880ab0f27ddf
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Wed Jan 16 18:54:18 2019 +0100
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Wed Jan 16 16:50:35 2019 -0500
     1.3 @@ -33,7 +33,7 @@
     1.4  
     1.5  subsection%unimportant \<open>More interesting properties of the norm\<close>
     1.6  
     1.7 -notation inner (infix "\<bullet>" 70)
     1.8 +unbundle inner_syntax
     1.9  
    1.10  text\<open>Equality of vectors in terms of \<^term>\<open>(\<bullet>)\<close> products.\<close>
    1.11