# HG changeset patch
# User chaieb
# Date 1248380709 -7200
# Node ID c6a045559ce6189a595231951edce1725aeb843b
# Parent  abda97d2deea79fed9a6e37cdbceb9eac8abaead
fixed proof --- fact_setprod removed for fact_altdef_nat

diff -r abda97d2deea -r c6a045559ce6 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Thu Jul 23 21:13:21 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Thu Jul 23 22:25:09 2009 +0200
@@ -2884,7 +2884,7 @@
 	  
 	  unfolding m h pochhammer_Suc_setprod
 	  apply (simp add: field_simps del: fact_Suc id_def)
-	  unfolding fact_setprod id_def
+	  unfolding fact_altdef_nat id_def
 	  unfolding of_nat_setprod
 	  unfolding setprod_timesf[symmetric]
 	  apply auto
@@ -3252,7 +3252,6 @@
 lemma F_1_0[simp]: "F [1] [] c = 1/(1 - fps_const c * X)"
 proof-
   let ?a = "(Abs_fps (\<lambda>n. 1)) oo (fps_const c * X)"
-  thm gp
   have th0: "(fps_const c * X) $ 0 = 0" by simp
   show ?thesis unfolding gp[OF th0, symmetric]
     by (auto simp add: fps_eq_iff pochhammer_fact[symmetric] fps_compose_nth power_mult_distrib cond_value_iff setsum_delta' cong del: if_weak_cong)