# HG changeset patch
# User wenzelm
# Date 976899570 -3600
# Node ID 26e4aecf32072de60a243c3cced4bfcbfbcccd03
# Parent  b619b56f562f8ed9e13ade75a403d1311361c2fc
tuned comment;

diff -r b619b56f562f -r 26e4aecf3207 src/HOL/PreList.thy
--- a/src/HOL/PreList.thy	Fri Dec 15 17:59:05 2000 +0100
+++ b/src/HOL/PreList.thy	Fri Dec 15 17:59:30 2000 +0100
@@ -21,7 +21,11 @@
 hide const Node Atom Leaf Numb Lim Funs Split Case
 
 
-(*belongs to theory Nat, but requires Datatype*)
+(* generic summation indexed over nat *)
+
+(*FIXME move to Ring_and_Field, when it is made part of main HOL (!?)*)
+(*FIXME port theorems from Algebra/abstract/NatSum*)
+
 consts
   Summation :: "(nat => 'a::{zero,plus}) => nat => 'a"
 primrec