# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1491294888 -7200
# Node ID a14fa655b48c9231eb6957d52d923416b2c01eeb
# Parent  9cdafcfb28bf64276c94a062a1ea69ce71e6e512
Tuned

diff -r 9cdafcfb28bf -r a14fa655b48c src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Tue Apr 04 09:01:42 2017 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Tue Apr 04 10:34:48 2017 +0200
@@ -1536,6 +1536,10 @@
 lemma fps_deriv_nth[simp]: "fps_deriv f $ n = of_nat (n +1) * f $ (n + 1)"
   by (simp add: fps_deriv_def)
 
+lemma fps_0th_higher_deriv: 
+  "(fps_deriv ^^ n) f $ 0 = (fact n * f $ n :: 'a :: {comm_ring_1, semiring_char_0})"
+  by (induction n arbitrary: f) (simp_all del: funpow.simps add: funpow_Suc_right algebra_simps)
+
 lemma fps_deriv_linear[simp]:
   "fps_deriv (fps_const (a::'a::comm_semiring_1) * f + fps_const b * g) =
     fps_const a * fps_deriv f + fps_const b * fps_deriv g"
diff -r 9cdafcfb28bf -r a14fa655b48c src/HOL/Number_Theory/Euclidean_Algorithm.thy
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Tue Apr 04 09:01:42 2017 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Tue Apr 04 10:34:48 2017 +0200
@@ -5,8 +5,8 @@
 section \<open>Abstract euclidean algorithm in euclidean (semi)rings\<close>
 
 theory Euclidean_Algorithm
-  imports "~~/src/HOL/GCD"
-    "~~/src/HOL/Number_Theory/Factorial_Ring"
+imports
+  "~~/src/HOL/Number_Theory/Factorial_Ring"
 begin
 
 subsection \<open>Generic construction of the (simple) euclidean algorithm\<close>
diff -r 9cdafcfb28bf -r a14fa655b48c src/HOL/Number_Theory/Factorial_Ring.thy
--- a/src/HOL/Number_Theory/Factorial_Ring.thy	Tue Apr 04 09:01:42 2017 +0200
+++ b/src/HOL/Number_Theory/Factorial_Ring.thy	Tue Apr 04 10:34:48 2017 +0200
@@ -8,7 +8,7 @@
 theory Factorial_Ring
 imports 
   Main
-  "~~/src/HOL/GCD"
+  GCD
   "~~/src/HOL/Library/Multiset"
 begin