author eberlm Tue, 04 Apr 2017 10:34:48 +0200 changeset 65398 a14fa655b48c parent 65397 9cdafcfb28bf child 65399 3f291f7a3646
Tuned
```--- 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)"

+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
```