doc-src/TutorialI/Misc/ROOT.ML
changeset 10538 d1bf9ca9008d
parent 9844 8016321c7de1
child 10543 8e4307d1207a
--- a/doc-src/TutorialI/Misc/ROOT.ML	Wed Nov 29 10:22:38 2000 +0100
+++ b/doc-src/TutorialI/Misc/ROOT.ML	Wed Nov 29 13:44:26 2000 +0100
@@ -4,9 +4,6 @@
 use_thy "case_exprs";
 use_thy "fakenat";
 use_thy "natsum";
-use_thy "arith1";
-use_thy "arith2";
-use_thy "arith3";
 use_thy "pairs";
 use_thy "types";
 use_thy "prime_def";