# HG changeset patch
# User huffman
# Date 1244043781 25200
# Node ID 8514775606e09fb193e6a1dce28a111e8d966b4c
# Parent  729d90a531e4b6e67e995c253886eeadc2348829
class real_inner derives from open_dist

diff -r 729d90a531e4 -r 8514775606e0 src/HOL/Library/Inner_Product.thy
--- 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"