--- a/src/HOL/Decision_Procs/Approximation.thy Thu Apr 03 17:56:08 2014 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Apr 03 18:24:08 2014 +0200
@@ -2678,16 +2678,16 @@
next
case (Cos a)
thus ?case
- by (auto intro!: derivative_intros
+ by (auto intro!: derivative_eq_intros
simp del: interpret_floatarith.simps(5)
simp add: interpret_floatarith_sin interpret_floatarith.simps(5)[of a])
next
case (Power a n)
thus ?case
- by (cases n) (auto intro!: derivative_intros simp del: power_Suc)
+ by (cases n) (auto intro!: derivative_eq_intros simp del: power_Suc simp add: real_of_nat_def)
next
case (Ln a)
- thus ?case by (auto intro!: derivative_intros simp add: divide_inverse)
+ thus ?case by (auto intro!: derivative_eq_intros simp add: divide_inverse)
next
case (Var i)
thus ?case using `n < length vs` by auto