# HG changeset patch
# User paulson
# Date 865509969 -7200
# Node ID 91a91790899a1c3904da94f559bdc83a5147a9d0
# Parent  6cc663f6d62e75b6f7bf37dbeceb7669b85c501e
Now loads theory Recdef

diff -r 6cc663f6d62e -r 91a91790899a src/HOL/ex/ROOT.ML
--- 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";