ex/NatSum.thy

--- a/ex/NatSum.thy	Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-(*  Title: 	HOL/ex/natsum.thy
-    ID:         $Id$
-    Author: 	Tobias Nipkow
-    Copyright   1994 TU Muenchen
-
-A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.
-*)
-
-NatSum = Arith +
-consts sum     :: "[nat=>nat, nat] => nat"
-rules  sum_0      "sum(f,0) = 0"
-       sum_Suc    "sum(f,Suc(n)) = f(n) + sum(f,n)"
-end