1.1 --- a/src/HOL/Library/Inner_Product.thy	Mon Sep 06 22:58:06 2010 +0200
     1.2 +++ b/src/HOL/Library/Inner_Product.thy	Tue Sep 07 10:05:19 2010 +0200
     1.3 @@ -307,7 +307,7 @@
     1.4    have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
     1.5      by (intro inner.FDERIV FDERIV_ident)
     1.6    have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"
     1.7 -    by (simp add: expand_fun_eq inner_commute)
     1.8 +    by (simp add: ext_iff inner_commute)
     1.9    have "0 < inner x x" using `x \<noteq> 0` by simp
    1.10    then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)"
    1.11      by (rule DERIV_real_sqrt)