src/HOL/Library/Inner_Product.thy
changeset 39198 f967a16dfcdd
parent 31590 776d6a4c1327
child 39302 d7728f65b353
--- 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)