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)"
```