| changeset 51525 | d3d170a2887f |
| parent 47217 | 501b9bbd0d6e |
| child 54230 | b1d955791529 |
| 51524:7cb5ac44ca9e | 51525:d3d170a2887f |
|---|---|
6 *) |
6 *) |
7 |
7 |
8 header{*Finite Summation and Infinite Series for Hyperreals*} |
8 header{*Finite Summation and Infinite Series for Hyperreals*} |
9 |
9 |
10 theory HSeries |
10 theory HSeries |
11 imports Series HSEQ |
11 imports HSEQ |
12 begin |
12 begin |
13 |
13 |
14 definition |
14 definition |
15 sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal" where |
15 sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal" where |
16 "sumhr = |
16 "sumhr = |