--- a/src/HOL/IsaMakefile Thu May 22 15:07:45 1997 +0200
+++ b/src/HOL/IsaMakefile Thu May 22 15:08:14 1997 +0200
@@ -200,7 +200,7 @@
## Miscellaneous examples
-EX_NAMES = String BT InSort Qsort Puzzle Primes NatSum MT
+EX_NAMES = Fib Primes NatSum String BT InSort Qsort Puzzle MT
EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
--- a/src/HOL/ex/ROOT.ML Thu May 22 15:07:45 1997 +0200
+++ b/src/HOL/ex/ROOT.ML Thu May 22 15:08:14 1997 +0200
@@ -10,6 +10,12 @@
writeln "Root file for HOL examples";
proof_timing := true;
+
+(**Some examples of recursive function definitions: the TFL package**)
+time_use_thy "Fib";
+time_use_thy "Primes";
+
+time_use_thy "NatSum";
time_use "cla.ML";
time_use "meson.ML";
time_use "mesontest.ML";
@@ -19,8 +25,7 @@
time_use_thy "InSort";
time_use_thy "Qsort";
time_use_thy "Puzzle";
-time_use_thy "Primes";
-time_use_thy "NatSum";
+
time_use "set.ML";
time_use_thy "MT";