class real_inner derives from open_dist
authorhuffman
Wed Jun 03 08:43:01 2009 -0700 (2009-06-03)
changeset 314148514775606e0
parent 31413 729d90a531e4
child 31415 80686a815b59
class real_inner derives from open_dist
src/HOL/Library/Inner_Product.thy
     1.1 --- a/src/HOL/Library/Inner_Product.thy	Wed Jun 03 07:44:56 2009 -0700
     1.2 +++ b/src/HOL/Library/Inner_Product.thy	Wed Jun 03 08:43:01 2009 -0700
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  subsection {* Real inner product spaces *}
     1.6  
     1.7 -class real_inner = real_vector + sgn_div_norm + dist_norm +
     1.8 +class real_inner = real_vector + sgn_div_norm + dist_norm + open_dist +
     1.9    fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
    1.10    assumes inner_commute: "inner x y = inner y x"
    1.11    and inner_left_distrib: "inner (x + y) z = inner x z + inner y z"