--- a/src/HOL/ex/ROOT.ML Fri Apr 16 19:04:17 2004 +0200
+++ b/src/HOL/ex/ROOT.ML Fri Apr 16 20:33:16 2004 +0200
@@ -33,7 +33,7 @@
no_document use_thy "List_Prefix";
time_use_thy "Exceptions";
-time_use_thy "IntRing";
+time_use_thy "Lagrange";
time_use_thy "set";
time_use_thy "MT";