--- 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
--- 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";