src/HOL/ex/ROOT.ML
changeset 3125 3f0ab2c306f7
parent 2987 becc227bad4d
child 3243 a42653373043
--- a/src/HOL/ex/ROOT.ML	Wed May 07 13:50:52 1997 +0200
+++ b/src/HOL/ex/ROOT.ML	Wed May 07 13:51:22 1997 +0200
@@ -16,22 +16,13 @@
 (** time_use "mesontest2.ML";  ULTRA SLOW **)
 time_use_thy "String";
 time_use_thy "BT";
-time_use_thy "Perm";
-time_use_thy "Comb";
 time_use_thy "InSort";
 time_use_thy "Qsort";
 time_use_thy "LexProd";
 time_use_thy "Puzzle";
-time_use_thy "Mutil";
 time_use_thy "Primes";
 time_use_thy "NatSum";
 time_use     "set.ML";
-time_use_thy "SList";
-time_use_thy "LFilter";
-time_use_thy "Acc";
-time_use_thy "PropLog";
-time_use_thy "Term";
-time_use_thy "Simult";
 time_use_thy "MT";
 
 writeln "END: Root file for HOL examples";