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";