New example: ex/Fib
authorpaulson
Thu May 22 15:08:14 1997 +0200 (1997-05-22)
changeset 32944c73b6508f53
parent 3293 c05f73cf3227
child 3295 c9c99aa082fb
New example: ex/Fib
src/HOL/IsaMakefile
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Thu May 22 15:07:45 1997 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu May 22 15:08:14 1997 +0200
     1.3 @@ -200,7 +200,7 @@
     1.4  
     1.5  ## Miscellaneous examples
     1.6  
     1.7 -EX_NAMES = String BT InSort Qsort Puzzle Primes NatSum MT
     1.8 +EX_NAMES = Fib Primes NatSum String BT InSort Qsort Puzzle MT
     1.9  
    1.10  EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
    1.11  	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
     2.1 --- a/src/HOL/ex/ROOT.ML	Thu May 22 15:07:45 1997 +0200
     2.2 +++ b/src/HOL/ex/ROOT.ML	Thu May 22 15:08:14 1997 +0200
     2.3 @@ -10,6 +10,12 @@
     2.4  
     2.5  writeln "Root file for HOL examples";
     2.6  proof_timing := true;
     2.7 +
     2.8 +(**Some examples of recursive function definitions: the TFL package**)
     2.9 +time_use_thy "Fib";
    2.10 +time_use_thy "Primes";
    2.11 +
    2.12 +time_use_thy "NatSum";
    2.13  time_use     "cla.ML";
    2.14  time_use     "meson.ML";
    2.15  time_use     "mesontest.ML";
    2.16 @@ -19,8 +25,7 @@
    2.17  time_use_thy "InSort";
    2.18  time_use_thy "Qsort";
    2.19  time_use_thy "Puzzle";
    2.20 -time_use_thy "Primes";
    2.21 -time_use_thy "NatSum";
    2.22 +
    2.23  time_use     "set.ML";
    2.24  time_use_thy "MT";
    2.25