src/HOL/Library/Formal_Power_Series.thy
changeset 31148 7ba7c1f8bc22
parent 31075 a9d6cf6de9a8
child 31199 10d413b08fa7
     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Thu May 14 08:22:07 2009 +0200
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Thu May 14 15:39:15 2009 +0200
     1.3 @@ -917,8 +917,7 @@
     1.4  proof-
     1.5    have eq: "(1 + X) * ?r = 1"
     1.6      unfolding minus_one_power_iff
     1.7 -    apply (auto simp add: ring_simps fps_eq_iff)
     1.8 -    by presburger+
     1.9 +    by (auto simp add: ring_simps fps_eq_iff)
    1.10    show ?thesis by (auto simp add: eq intro: fps_inverse_unique)
    1.11  qed
    1.12  
    1.13 @@ -2286,9 +2285,7 @@
    1.14    (is "inverse ?l = ?r")
    1.15  proof-
    1.16    have th: "?l * ?r = 1"
    1.17 -    apply (auto simp add: ring_simps fps_eq_iff X_mult_nth  minus_one_power_iff)
    1.18 -    apply presburger+
    1.19 -    done
    1.20 +    by (auto simp add: ring_simps fps_eq_iff minus_one_power_iff)
    1.21    have th': "?l $ 0 \<noteq> 0" by (simp add: )
    1.22    from fps_inverse_unique[OF th' th] show ?thesis .
    1.23  qed