# HG changeset patch
# User hoelzl
# Date 1396542248 -7200
# Node ID 5a50109d51ab93144c0fcc57fb6dbc30c45ce98e
# Parent  0556204bc230587a5f626a46cd3e5a87a4131402
fix #0556204bc230

diff -r 0556204bc230 -r 5a50109d51ab src/HOL/Decision_Procs/Approximation.thy
--- 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