changeset 9942 | 87f0809a06a9 |
parent 9840 | 9dfcb0224f8c |
child 10052 | 5fa8d8d5c852 |
--- a/src/HOL/ex/ROOT.ML Tue Sep 12 22:13:23 2000 +0200 +++ b/src/HOL/ex/ROOT.ML Wed Sep 13 18:45:10 2000 +0200 @@ -6,9 +6,6 @@ (*some examples of recursive function definitions: the TFL package*) time_use_thy "Recdefs"; -time_use_thy "Primes"; -time_use_thy "Fib"; -with_path "../Induct" time_use_thy "Factorization"; time_use_thy "Primrec"; time_use_thy "NatSum";