--- a/src/HOL/Library/Inner_Product.thy Wed Jun 03 07:44:56 2009 -0700
+++ b/src/HOL/Library/Inner_Product.thy Wed Jun 03 08:43:01 2009 -0700
@@ -10,7 +10,7 @@
subsection {* Real inner product spaces *}
-class real_inner = real_vector + sgn_div_norm + dist_norm +
+class real_inner = real_vector + sgn_div_norm + dist_norm + open_dist +
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"