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