src/HOL/Library/Formal_Power_Series.thy
changeset 59741 5b762cd73a8e
parent 59730 b7c394c7a619
child 59815 cce82e360c2f
--- a/src/HOL/Library/Formal_Power_Series.thy	Tue Mar 17 17:45:03 2015 +0000
+++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Mar 18 14:13:27 2015 +0000
@@ -8,8 +8,6 @@
 imports Complex_Main
 begin
 
-lemmas fact_Suc = fact.simps(2)
-
 subsection {* The type of formal power series*}
 
 typedef 'a fps = "{f :: nat \<Rightarrow> 'a. True}"
@@ -594,7 +592,7 @@
       fix n :: nat
       assume nn0: "n \<ge> n0"
       then have thnn0: "(1/2)^n \<le> (1/2 :: real)^n0"
-        by (auto intro: power_decreasing)
+        by (simp add: divide_simps)
       {
         assume "?s n = a"
         then have "dist (?s n) a < r"
@@ -612,9 +610,9 @@
           by (auto simp: fps_sum_rep_nth not_le k_def fps_eq_iff
               split: split_if_asm intro: LeastI2_ex)
         then have "dist (?s n) a < (1/2)^n"
-          unfolding dth by (auto intro: power_strict_decreasing)
+          unfolding dth by (simp add: divide_simps)
         also have "\<dots> \<le> (1/2)^n0"
-          using nn0 by (auto intro: power_decreasing)
+          using nn0 by (simp add: divide_simps)
         also have "\<dots> < r"
           using n0 by simp
         finally have "dist (?s n) a < r" .