equal
deleted
inserted
replaced
4 Description : MacLaurin series |
4 Description : MacLaurin series |
5 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
5 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
6 *) |
6 *) |
7 |
7 |
8 theory MacLaurin |
8 theory MacLaurin |
9 import Log |
9 imports Log |
10 begin |
10 begin |
11 |
11 |
12 lemma sumr_offset: "sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f" |
12 lemma sumr_offset: "sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f" |
13 by (induct_tac "n", auto) |
13 by (induct_tac "n", auto) |
14 |
14 |