--- a/src/HOL/Decision_Procs/Approximation.thy Thu Apr 03 17:16:02 2014 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Apr 03 17:56:08 2014 +0200
@@ -2674,24 +2674,24 @@
proof (induct f arbitrary: x)
case (Inverse a)
thus ?case
- by (auto intro!: DERIV_intros simp add: algebra_simps power2_eq_square)
+ by (auto intro!: derivative_eq_intros simp add: algebra_simps power2_eq_square)
next
case (Cos a)
thus ?case
- by (auto intro!: DERIV_intros
+ by (auto intro!: derivative_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!: DERIV_intros simp del: power_Suc)
+ by (cases n) (auto intro!: derivative_intros simp del: power_Suc)
next
case (Ln a)
- thus ?case by (auto intro!: DERIV_intros simp add: divide_inverse)
+ thus ?case by (auto intro!: derivative_intros simp add: divide_inverse)
next
case (Var i)
thus ?case using `n < length vs` by auto
-qed (auto intro!: DERIV_intros)
+qed (auto intro!: derivative_eq_intros)
declare approx.simps[simp del]