diff -r 375db037f4d2 -r 341c83339aeb src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Sat Aug 29 14:31:39 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Mon Aug 31 14:09:42 2009 +0200
@@ -633,8 +633,7 @@
 	    by (auto simp add: inverse_eq_divide power_divide)
 
 	  from k have kn: "k > n"
-	    apply (simp add: leastP_def setge_def fps_sum_rep_nth)
-	    by (cases "k \<le> n", auto)
+	    by (simp add: leastP_def setge_def fps_sum_rep_nth split:split_if_asm)
 	  then have "dist (?s n) a < (1/2)^n" unfolding dth
 	    by (auto intro: power_strict_decreasing)
 	  also have "\<dots> <= (1/2)^n0" using nn0
@@ -1244,10 +1243,9 @@
     {assume n0: "n \<noteq> 0"
       then have u: "{0} \<union> ({1} \<union> {2..n}) = {0..n}" "{1}\<union>{2..n} = {1..n}"
 	"{0..n - 1}\<union>{n} = {0..n}"
-	apply (simp_all add: expand_set_eq) by presburger+
+	by (auto simp: expand_set_eq)
       have d: "{0} \<inter> ({1} \<union> {2..n}) = {}" "{1} \<inter> {2..n} = {}"
-	"{0..n - 1}\<inter>{n} ={}" using n0
-	by (simp_all add: expand_set_eq, presburger+)
+	"{0..n - 1}\<inter>{n} ={}" using n0 by simp_all
       have f: "finite {0}" "finite {1}" "finite {2 .. n}"
 	"finite {0 .. n - 1}" "finite {n}" by simp_all
     have "((1 - ?X) * ?sa) $ n = setsum (\<lambda>i. (1 - ?X)$ i * ?sa $ (n - i)) {0 .. n}"