--- a/src/HOL/Analysis/Inner_Product.thy Wed Jan 16 18:54:18 2019 +0100
+++ b/src/HOL/Analysis/Inner_Product.thy Wed Jan 16 16:50:35 2019 -0500
@@ -462,4 +462,12 @@
lemmas has_derivative_norm = GDERIV_norm [unfolded gderiv_def]
+bundle inner_syntax begin
+notation inner (infix "\<bullet>" 70)
end
+
+bundle no_inner_syntax begin
+no_notation inner (infix "\<bullet>" 70)
+end
+
+end
--- a/src/HOL/Analysis/Linear_Algebra.thy Wed Jan 16 18:54:18 2019 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy Wed Jan 16 16:50:35 2019 -0500
@@ -33,7 +33,7 @@
subsection%unimportant \<open>More interesting properties of the norm\<close>
-notation inner (infix "\<bullet>" 70)
+unbundle inner_syntax
text\<open>Equality of vectors in terms of \<^term>\<open>(\<bullet>)\<close> products.\<close>