--- a/src/HOL/IsaMakefile Tue May 23 18:29:17 2000 +0200
+++ b/src/HOL/IsaMakefile Wed May 24 12:21:26 2000 +0200
@@ -410,7 +410,7 @@
HOL-ex: HOL $(LOG)/HOL-ex.gz
$(LOG)/HOL-ex.gz: $(OUT)/HOL ex/AVL.ML ex/AVL.thy ex/BT.ML ex/BT.thy \
- ex/InSort.ML ex/InSort.thy ex/MT.ML ex/MT.thy ex/NatSum.ML \
+ ex/InSort.ML ex/InSort.thy ex/MT.ML ex/MT.thy ex/NatSum.ML ex/NatSum.thy \
ex/Fib.ML ex/Fib.thy ex/Primes.ML ex/Primes.thy \
ex/Factorization.ML ex/Factorization.thy \
ex/Primrec.ML ex/Primrec.thy \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/NatSum.thy Wed May 24 12:21:26 2000 +0200
@@ -0,0 +1,1 @@
+NatSum = Main
--- a/src/HOL/ex/ROOT.ML Tue May 23 18:29:17 2000 +0200
+++ b/src/HOL/ex/ROOT.ML Wed May 24 12:21:26 2000 +0200
@@ -17,7 +17,7 @@
with_path "../Induct" use_thy "Factorization";
time_use_thy "Primrec";
-time_use "NatSum";
+time_use_thy "NatSum";
time_use "cla.ML";
time_use "meson.ML";
time_use "mesontest.ML";