--- a/src/HOL/ex/Formal_Power_Series_Examples.thy Thu May 28 13:43:45 2009 -0700
+++ b/src/HOL/ex/Formal_Power_Series_Examples.thy Thu May 28 13:52:13 2009 -0700
@@ -11,7 +11,7 @@
section{* The generalized binomial theorem *}
lemma gbinomial_theorem:
- "((a::'a::{ring_char_0, field, division_by_zero})+b) ^ n = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
+ "((a::'a::{field_char_0, division_by_zero})+b) ^ n = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
proof-
from E_add_mult[of a b]
have "(E (a + b)) $ n = (E a * E b)$n" by simp
@@ -38,7 +38,7 @@
by (simp add: fps_binomial_def)
lemma fps_binomial_ODE_unique:
- fixes c :: "'a::{field, ring_char_0}"
+ fixes c :: "'a::field_char_0"
shows "fps_deriv a = (fps_const c * a) / (1 + X) \<longleftrightarrow> a = fps_const (a$0) * fps_binomial c"
(is "?lhs \<longleftrightarrow> ?rhs")
proof-
@@ -302,4 +302,4 @@
finally show ?thesis .
qed
-end
\ No newline at end of file
+end