| changeset 44233 | aa74ce315bae |
| parent 44126 | ce44e70d0c47 |
| child 44282 | f0de18b62d63 |
--- a/src/HOL/Library/Inner_Product.thy Tue Aug 16 13:07:52 2011 -0700 +++ b/src/HOL/Library/Inner_Product.thy Tue Aug 16 09:31:23 2011 -0700 @@ -175,6 +175,8 @@ bounded_linear "\<lambda>y::'a::real_inner. inner x y" by (rule inner.bounded_linear_right) +declare inner.isCont [simp] + subsection {* Class instances *}