equal
deleted
inserted
replaced
19 |
19 |
20 (*belongs to theory Datatype_Universe; hides popular names *) |
20 (*belongs to theory Datatype_Universe; hides popular names *) |
21 hide const Node Atom Leaf Numb Lim Funs Split Case |
21 hide const Node Atom Leaf Numb Lim Funs Split Case |
22 |
22 |
23 |
23 |
24 (*belongs to theory Nat, but requires Datatype*) |
24 (* generic summation indexed over nat *) |
|
25 |
|
26 (*FIXME move to Ring_and_Field, when it is made part of main HOL (!?)*) |
|
27 (*FIXME port theorems from Algebra/abstract/NatSum*) |
|
28 |
25 consts |
29 consts |
26 Summation :: "(nat => 'a::{zero,plus}) => nat => 'a" |
30 Summation :: "(nat => 'a::{zero,plus}) => nat => 'a" |
27 primrec |
31 primrec |
28 "Summation f 0 = 0" |
32 "Summation f 0 = 0" |
29 "Summation f (Suc n) = Summation f n + f n" |
33 "Summation f (Suc n) = Summation f n + f n" |