# HG changeset patch
# User paulson
# Date 959078196 -7200
# Node ID de96f2982d2c0e57c50f6b9dfcfddbfb4785b302
# Parent  c1d0f74957142f745dbf9b695318d4fabe8f69de
theory file NatSum.thy no longer needed

diff -r c1d0f7495714 -r de96f2982d2c src/HOL/ex/NatSum.thy
--- a/src/HOL/ex/NatSum.thy	Tue May 23 12:35:57 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +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 = Main +
-consts sum     :: [nat=>nat, nat] => nat
-primrec 
-  sum_0    "sum f 0 = 0"
-  sum_Suc  "sum f (Suc n) = f(n) + sum f n"
-
-end
diff -r c1d0f7495714 -r de96f2982d2c src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Tue May 23 12:35:57 2000 +0200
+++ b/src/HOL/ex/ROOT.ML	Tue May 23 12:36:36 2000 +0200
@@ -17,7 +17,7 @@
 with_path "../Induct" use_thy "Factorization";
 time_use_thy "Primrec";
 
-time_use_thy "NatSum";
+time_use     "NatSum";
 time_use     "cla.ML";
 time_use     "meson.ML";
 time_use     "mesontest.ML";