src/HOL/Library/Formal_Power_Series.thy

   obtain k::nat where k: "real k > max 0 (- log y x) + 1" by blast
   from k have kp: "k > 0" by simp
   from k have "real k > - log y x" by simp
   then have "ln y * real k > - ln x" unfolding log_def
     using ln_gt_zero_iff[OF yp] y1
-    by (simp add: minus_divide_left field_simps del:minus_divide_left[symmetric] )
+    by (simp add: minus_divide_left field_eq_simps del:minus_divide_left[symmetric] )
   then have "ln y * real k + ln x > 0" by simp
   then have "exp (real k * ln y + ln x) > exp 0"
     by (simp add: mult_ac)
   then have "y ^ k * x > 1"
     unfolding exp_zero exp_add exp_real_of_nat_mult
     exp_ln[OF xp] exp_ln[OF yp] by simp
   then have "x > (1/y)^k" using yp 
-    by (simp add: field_simps nonzero_power_divide )
+    by (simp add: field_eq_simps nonzero_power_divide )
   then show ?thesis using kp by blast
 qed
 lemma X_nth[simp]: "X$n = (if n = 1 then 1 else 0)" by (simp add: X_def)
 lemma X_power_nth[simp]: "(X^k) $n = (if n = k then 1 else (0::'a::comm_ring_1))"
   by (simp add: X_power_iff)