equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 header{*Finite Summation and Infinite Series*} |
8 header{*Finite Summation and Infinite Series*} |
9 |
9 |
10 theory Series |
10 theory Series |
11 import SEQ Lim |
11 imports SEQ Lim |
12 begin |
12 begin |
13 |
13 |
14 syntax sumr :: "[nat,nat,(nat=>real)] => real" |
14 syntax sumr :: "[nat,nat,(nat=>real)] => real" |
15 translations |
15 translations |
16 "sumr m n f" => "setsum (f::nat=>real) (atLeastLessThan m n)" |
16 "sumr m n f" => "setsum (f::nat=>real) (atLeastLessThan m n)" |