src/HOL/Library/Inner_Product.thy

 imports Complex_Main FrechetDeriv
 begin
 
 subsection {* Real inner product spaces *}
 
-class real_inner = real_vector + sgn_div_norm +
+class real_inner = real_vector + sgn_div_norm + dist_norm +
   fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
   assumes inner_commute: "inner x y = inner y x"
   and inner_left_distrib: "inner (x + y) z = inner x z + inner y z"
   and inner_scaleR_left: "inner (scaleR r x) y = r * (inner x y)"
   and inner_ge_zero [simp]: "0 \<le> inner x x"