src/HOL/Analysis/Inner_Product.thy
changeset 68623 b942da0962c2
parent 68617 75129a73aca3
child 69064 5840724b1d71
     1.1 --- a/src/HOL/Analysis/Inner_Product.thy	Fri Jul 13 15:00:38 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Inner_Product.thy	Fri Jul 13 15:42:18 2018 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4  setup \<open>Sign.add_const_constraint
     1.5    (@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"})\<close>
     1.6  
     1.7 -class%important real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
     1.8 +class real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
     1.9    fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
    1.10    assumes inner_commute: "inner x y = inner y x"
    1.11    and inner_add_left: "inner (x + y) z = inner x z + inner y z"