# HG changeset patch
# User haftmann
# Date 1272032245 -7200
# Node ID 4da07afb065bfdcdc6d526206f1f98f6eb127fe1
# Parent  bbcfeddeafbb76412c88c56541b51d889a91a71c
epheremal replacement of field_simps by field_eq_simps

diff -r bbcfeddeafbb -r 4da07afb065b src/HOL/Library/Binomial.thy
--- 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 ..
diff -r bbcfeddeafbb -r 4da07afb065b src/HOL/Library/Formal_Power_Series.thy
--- 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)
diff -r bbcfeddeafbb -r 4da07afb065b src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- 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