src/HOL/Analysis/Inner_Product.thy
changeset 68617 75129a73aca3
parent 68611 4bc4b5c0ccfc
child 68623 b942da0962c2
     1.1 --- a/src/HOL/Analysis/Inner_Product.thy	Wed Jul 11 23:24:25 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Inner_Product.thy	Thu Jul 12 11:23:46 2018 +0200
     1.3 @@ -274,7 +274,7 @@
     1.4  
     1.5  subsection \<open>Class instances\<close>
     1.6  
     1.7 -instantiation%important real :: real_inner
     1.8 +instantiation real :: real_inner
     1.9  begin
    1.10  
    1.11  definition inner_real_def [simp]: "inner = ( * )"
    1.12 @@ -303,7 +303,7 @@
    1.13      and real_inner_1_right[simp]: "inner x 1 = x"
    1.14    by simp_all
    1.15  
    1.16 -instantiation%important complex :: real_inner
    1.17 +instantiation complex :: real_inner
    1.18  begin
    1.19  
    1.20  definition inner_complex_def: