# HG changeset patch
# User immler
# Date 1547675435 18000
# Node ID fc252acb7100312664eb3230d6de03fbb3a318d5
# Parent  cc47e7e06f383419ec8fcc465b8ea4cfe5247bc8
bundle syntax for inner

diff -r cc47e7e06f38 -r fc252acb7100 src/HOL/Analysis/Inner_Product.thy
--- 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
diff -r cc47e7e06f38 -r fc252acb7100 src/HOL/Analysis/Linear_Algebra.thy
--- 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>