--- a/src/HOL/Induct/ROOT.ML Sat Feb 03 15:22:57 2001 +0100
+++ b/src/HOL/Induct/ROOT.ML Sat Feb 03 17:40:16 2001 +0100
@@ -1,16 +1,12 @@
-(* Title: HOL/Induct/ROOT.ML
-Examples of Inductive and Coinductive Definitions.
-*)
-
+time_use_thy "Mutil";
+time_use_thy "Term";
+time_use_thy "ABexp";
+time_use_thy "Tree";
time_use_thy "Sigma_Algebra";
time_use_thy "Perm";
time_use_thy "Comb";
-time_use_thy "Mutil";
time_use_thy "PropLog";
time_use_thy "SList";
time_use_thy "LFilter";
-time_use_thy "Term";
-time_use_thy "ABexp";
time_use_thy "Exp";
-time_use_thy "Tree";