doc-src/TutorialI/Types/ROOT.ML
changeset 10538 d1bf9ca9008d
parent 10362 c6b197ccf1f1
child 10579 1db42f739ee7
--- a/doc-src/TutorialI/Types/ROOT.ML	Wed Nov 29 10:22:38 2000 +0100
+++ b/doc-src/TutorialI/Types/ROOT.ML	Wed Nov 29 13:44:26 2000 +0100
@@ -1,4 +1,5 @@
 use "../settings.ML";
+use_thy "Pairs";
 use_thy "Typedef";
 use_thy "Overloading0";
 use_thy "Overloading2";