src/HOL/PreList.thy
changeset 10680 26e4aecf3207
parent 10671 ac6b3b671198
child 10733 59f82484e000
     1.1 --- a/src/HOL/PreList.thy	Fri Dec 15 17:59:05 2000 +0100
     1.2 +++ b/src/HOL/PreList.thy	Fri Dec 15 17:59:30 2000 +0100
     1.3 @@ -21,7 +21,11 @@
     1.4  hide const Node Atom Leaf Numb Lim Funs Split Case
     1.5  
     1.6  
     1.7 -(*belongs to theory Nat, but requires Datatype*)
     1.8 +(* generic summation indexed over nat *)
     1.9 +
    1.10 +(*FIXME move to Ring_and_Field, when it is made part of main HOL (!?)*)
    1.11 +(*FIXME port theorems from Algebra/abstract/NatSum*)
    1.12 +
    1.13  consts
    1.14    Summation :: "(nat => 'a::{zero,plus}) => nat => 'a"
    1.15  primrec