# HG changeset patch
# User paulson
# Date 864306494 -7200
# Node ID 4c73b6508f535603e62969bb73bd2799e9288a1e
# Parent  c05f73cf32275ff8864de411dbcda960adf5f154
New example: ex/Fib

diff -r c05f73cf3227 -r 4c73b6508f53 src/HOL/IsaMakefile
--- 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)
diff -r c05f73cf3227 -r 4c73b6508f53 src/HOL/ex/ROOT.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";