# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1396542405 -3600
# Node ID 5fdcfffcc72e5901bc9ca3c86b4c2002d8b58b7b
# Parent  8e7052e9fda43f3231285b613b593762fc67c311# Parent  5a50109d51ab93144c0fcc57fb6dbc30c45ce98e
Merge

diff -r 8e7052e9fda4 -r 5fdcfffcc72e src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Thu Apr 03 17:26:04 2014 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Apr 03 17:26:45 2014 +0100
@@ -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