src/HOL/Library/Formal_Power_Series.thy
changeset 36309 4da07afb065b
parent 35175 61255c81da01
child 36311 ed3a87a7f977
     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Fri Apr 23 16:17:24 2010 +0200
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Apr 23 16:17:25 2010 +0200
     1.3 @@ -586,7 +586,7 @@
     1.4    from k have "real k > - log y x" by simp
     1.5    then have "ln y * real k > - ln x" unfolding log_def
     1.6      using ln_gt_zero_iff[OF yp] y1
     1.7 -    by (simp add: minus_divide_left field_simps del:minus_divide_left[symmetric] )
     1.8 +    by (simp add: minus_divide_left field_eq_simps del:minus_divide_left[symmetric] )
     1.9    then have "ln y * real k + ln x > 0" by simp
    1.10    then have "exp (real k * ln y + ln x) > exp 0"
    1.11      by (simp add: mult_ac)
    1.12 @@ -594,7 +594,7 @@
    1.13      unfolding exp_zero exp_add exp_real_of_nat_mult
    1.14      exp_ln[OF xp] exp_ln[OF yp] by simp
    1.15    then have "x > (1/y)^k" using yp 
    1.16 -    by (simp add: field_simps nonzero_power_divide )
    1.17 +    by (simp add: field_eq_simps nonzero_power_divide )
    1.18    then show ?thesis using kp by blast
    1.19  qed
    1.20  lemma X_nth[simp]: "X$n = (if n = 1 then 1 else 0)" by (simp add: X_def)