src/HOL/ex/ROOT.ML
changeset 3404 91a91790899a
parent 3337 c056d328aa0e
child 4449 df30e75f670f
--- a/src/HOL/ex/ROOT.ML	Thu Jun 05 13:22:25 1997 +0200
+++ b/src/HOL/ex/ROOT.ML	Thu Jun 05 13:26:09 1997 +0200
@@ -12,6 +12,7 @@
 proof_timing := true;
 
 (**Some examples of recursive function definitions: the TFL package**)
+time_use_thy "Recdef";
 time_use_thy "Fib";
 time_use_thy "Primes";
 time_use_thy "Primrec";