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