bundle syntax for inner
authorimmler
Wed Jan 16 16:50:35 2019 -0500 (4 months ago)
changeset 69674fc252acb7100
parent 69673 cc47e7e06f38
child 69675 880ab0f27ddf
bundle syntax for inner
src/HOL/Analysis/Inner_Product.thy
src/HOL/Analysis/Linear_Algebra.thy
     1.1 --- a/src/HOL/Analysis/Inner_Product.thy	Wed Jan 16 18:54:18 2019 +0100
     1.2 +++ b/src/HOL/Analysis/Inner_Product.thy	Wed Jan 16 16:50:35 2019 -0500
     1.3 @@ -462,4 +462,12 @@
     1.4  
     1.5  lemmas has_derivative_norm = GDERIV_norm [unfolded gderiv_def]
     1.6  
     1.7 +bundle inner_syntax begin
     1.8 +notation inner (infix "\<bullet>" 70)
     1.9  end
    1.10 +
    1.11 +bundle no_inner_syntax begin
    1.12 +no_notation inner (infix "\<bullet>" 70)
    1.13 +end
    1.14 +
    1.15 +end
     2.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Wed Jan 16 18:54:18 2019 +0100
     2.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Wed Jan 16 16:50:35 2019 -0500
     2.3 @@ -33,7 +33,7 @@
     2.4  
     2.5  subsection%unimportant \<open>More interesting properties of the norm\<close>
     2.6  
     2.7 -notation inner (infix "\<bullet>" 70)
     2.8 +unbundle inner_syntax
     2.9  
    2.10  text\<open>Equality of vectors in terms of \<^term>\<open>(\<bullet>)\<close> products.\<close>
    2.11