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