Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Merge
authorpaulson <lp15@cam.ac.uk>
Thu, 03 Apr 2014 17:26:45 +0100
changeset 56384 5fdcfffcc72e
parent 56383 8e7052e9fda4 (current diff)
parent 56382 5a50109d51ab (diff)
child 56396 91a8561a8e35
Merge
--- 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
isabelle