--- a/src/HOL/Library/Binomial.thy Fri Apr 23 16:17:24 2010 +0200
+++ b/src/HOL/Library/Binomial.thy Fri Apr 23 16:17:25 2010 +0200
@@ -391,13 +391,13 @@
assumes kn: "k \<le> n"
shows "(of_nat (n choose k) :: 'a::field_char_0) = of_nat (fact n) / (of_nat (fact k) * of_nat (fact (n - k)))"
using binomial_fact_lemma[OF kn]
- by (simp add: field_simps of_nat_mult[symmetric])
+ by (simp add: field_eq_simps of_nat_mult [symmetric])
lemma binomial_gbinomial: "of_nat (n choose k) = of_nat n gchoose k"
proof-
{assume kn: "k > n"
from kn binomial_eq_0[OF kn] have ?thesis
- by (simp add: gbinomial_pochhammer field_simps
+ by (simp add: gbinomial_pochhammer field_eq_simps
pochhammer_of_nat_eq_0_iff)}
moreover
{assume "k=0" then have ?thesis by simp}
@@ -420,7 +420,7 @@
from eq[symmetric]
have ?thesis using kn
apply (simp add: binomial_fact[OF kn, where ?'a = 'a]
- gbinomial_pochhammer field_simps pochhammer_Suc_setprod)
+ gbinomial_pochhammer field_eq_simps pochhammer_Suc_setprod)
apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc)
unfolding setprod_Un_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]
unfolding mult_assoc[symmetric]
@@ -449,7 +449,7 @@
have "?r = ((- 1) ^n * pochhammer (- a) n / of_nat (fact n)) * (of_nat n - (- a + of_nat n))"
unfolding gbinomial_pochhammer
pochhammer_Suc fact_Suc of_nat_mult right_diff_distrib power_Suc
- by (simp add: field_simps del: of_nat_Suc)
+ by (simp add: field_eq_simps del: of_nat_Suc)
also have "\<dots> = ?l" unfolding gbinomial_pochhammer
by (simp add: ring_simps)
finally show ?thesis ..
--- a/src/HOL/Library/Formal_Power_Series.thy Fri Apr 23 16:17:24 2010 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Fri Apr 23 16:17:25 2010 +0200
@@ -586,7 +586,7 @@
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)
@@ -594,7 +594,7 @@
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)
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Apr 23 16:17:24 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Apr 23 16:17:25 2010 +0200
@@ -2780,7 +2780,7 @@
from geometric_sum[OF x1, of "Suc n", unfolded x1']
have "(- (1 - x)) * setsum (\<lambda>i. x^i) {0 .. n} = - (1 - x^(Suc n))"
unfolding atLeastLessThanSuc_atLeastAtMost
- using x1' apply (auto simp only: field_simps)
+ using x1' apply (auto simp only: field_eq_simps)
apply (simp add: ring_simps)
done
then have ?thesis by (simp add: ring_simps) }
@@ -2815,7 +2815,7 @@
{assume x: "x = 1" hence ?thesis by simp}
moreover
{assume x: "x \<noteq> 1" hence nz: "1 - x \<noteq> 0" by simp
- from sum_gp_multiplied[OF nm, of x] nz have ?thesis by (simp add: field_simps)}
+ from sum_gp_multiplied[OF nm, of x] nz have ?thesis by (simp add: field_eq_simps)}
ultimately have ?thesis by metis
}
ultimately show ?thesis by metis