src/HOL/Library/Formal_Power_Series.thy
changeset 59867 58043346ca64
parent 59862 44b3f4fa33ca
child 60017 b785d6d06430
     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Tue Mar 31 16:49:41 2015 +0100
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Tue Mar 31 21:54:32 2015 +0200
     1.3 @@ -3628,7 +3628,7 @@
     1.4  
     1.5  subsection {* Hypergeometric series *}
     1.6  
     1.7 -definition "F as bs (c::'a::{field_char_0,field_inverse_zero}) =
     1.8 +definition "F as bs (c::'a::{field_char_0,field}) =
     1.9    Abs_fps (\<lambda>n. (foldl (\<lambda>r a. r* pochhammer a n) 1 as * c^n) /
    1.10      (foldl (\<lambda>r b. r * pochhammer b n) 1 bs * of_nat (fact n)))"
    1.11  
    1.12 @@ -3711,11 +3711,11 @@
    1.13    by (simp add: fps_eq_iff fps_integral_def)
    1.14  
    1.15  lemma F_minus_nat:
    1.16 -  "F [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0,field_inverse_zero}) $ k =
    1.17 +  "F [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0,field}) $ k =
    1.18      (if k \<le> n then
    1.19        pochhammer (- of_nat n) k * c ^ k / (pochhammer (- of_nat (n + m)) k * of_nat (fact k))
    1.20       else 0)"
    1.21 -  "F [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0,field_inverse_zero}) $ k =
    1.22 +  "F [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0,field}) $ k =
    1.23      (if k \<le> m then
    1.24        pochhammer (- of_nat m) k * c ^ k / (pochhammer (- of_nat (m + n)) k * of_nat (fact k))
    1.25       else 0)"