ex/ROOT.ML
changeset 208 deec279dda0a
parent 195 df6b3bd14dcb
child 222 c789c7441119
--- a/ex/ROOT.ML	Wed Feb 01 17:18:00 1995 +0100
+++ b/ex/ROOT.ML	Fri Feb 03 16:19:45 1995 +0100
@@ -14,6 +14,7 @@
 time_use     "ex/cla.ML";
 time_use     "ex/meson.ML";
 time_use     "ex/mesontest.ML";
+time_use_thy "String";
 time_use_thy "InSort";
 time_use_thy "Qsort";
 time_use_thy "LexProd";