--- 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"
--- 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>
--- 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