--- a/src/HOL/Library/Formal_Power_Series.thy Thu May 14 08:22:07 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Thu May 14 15:39:15 2009 +0200
@@ -917,8 +917,7 @@
proof-
have eq: "(1 + X) * ?r = 1"
unfolding minus_one_power_iff
- apply (auto simp add: ring_simps fps_eq_iff)
- by presburger+
+ by (auto simp add: ring_simps fps_eq_iff)
show ?thesis by (auto simp add: eq intro: fps_inverse_unique)
qed
@@ -2286,9 +2285,7 @@
(is "inverse ?l = ?r")
proof-
have th: "?l * ?r = 1"
- apply (auto simp add: ring_simps fps_eq_iff X_mult_nth minus_one_power_iff)
- apply presburger+
- done
+ by (auto simp add: ring_simps fps_eq_iff minus_one_power_iff)
have th': "?l $ 0 \<noteq> 0" by (simp add: )
from fps_inverse_unique[OF th' th] show ?thesis .
qed