changeset 31289 | 847f00f435d4 |
parent 30729 | 461ee3e49ad3 |
child 31414 | 8514775606e0 |
--- a/src/HOL/Library/Inner_Product.thy Thu May 28 14:36:21 2009 -0700 +++ b/src/HOL/Library/Inner_Product.thy Thu May 28 17:00:02 2009 -0700 @@ -10,7 +10,7 @@ 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"