fixed proof --- fact_setprod removed for fact_altdef_nat
authorchaieb
Thu Jul 23 22:25:09 2009 +0200 (2009-07-23)
changeset 32162c6a045559ce6
parent 32161 abda97d2deea
child 32163 8aee65c5e33c
fixed proof --- fact_setprod removed for fact_altdef_nat
src/HOL/Library/Formal_Power_Series.thy
     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Thu Jul 23 21:13:21 2009 +0200
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Thu Jul 23 22:25:09 2009 +0200
     1.3 @@ -2884,7 +2884,7 @@
     1.4  	  
     1.5  	  unfolding m h pochhammer_Suc_setprod
     1.6  	  apply (simp add: field_simps del: fact_Suc id_def)
     1.7 -	  unfolding fact_setprod id_def
     1.8 +	  unfolding fact_altdef_nat id_def
     1.9  	  unfolding of_nat_setprod
    1.10  	  unfolding setprod_timesf[symmetric]
    1.11  	  apply auto
    1.12 @@ -3252,7 +3252,6 @@
    1.13  lemma F_1_0[simp]: "F [1] [] c = 1/(1 - fps_const c * X)"
    1.14  proof-
    1.15    let ?a = "(Abs_fps (\<lambda>n. 1)) oo (fps_const c * X)"
    1.16 -  thm gp
    1.17    have th0: "(fps_const c * X) $ 0 = 0" by simp
    1.18    show ?thesis unfolding gp[OF th0, symmetric]
    1.19      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)