doc-src/TutorialI/Misc/ROOT.ML
changeset 10978 5eebea8f359f
parent 10543 8e4307d1207a
child 11203 881222d48777
--- a/doc-src/TutorialI/Misc/ROOT.ML	Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/Misc/ROOT.ML	Thu Jan 25 15:31:31 2001 +0100
@@ -11,3 +11,4 @@
 use_thy "simp";
 use_thy "Itrev";
 use_thy "AdvancedInd";
+use_thy "appendix";