no_document use_thy "While_Combinator";
authorwenzelm
Tue, 08 Jan 2002 20:44:57 +0100
changeset 12675 25f1e89b5012
parent 12674 106d62d106fc
child 12676 99e7b2045d8f
no_document use_thy "While_Combinator";
doc-src/TutorialI/Advanced/ROOT.ML
--- a/doc-src/TutorialI/Advanced/ROOT.ML	Tue Jan 08 18:08:02 2002 +0100
+++ b/doc-src/TutorialI/Advanced/ROOT.ML	Tue Jan 08 20:44:57 2002 +0100
@@ -1,4 +1,5 @@
 use "../settings.ML";
+no_document use_thy "While_Combinator";
 use_thy "simp";
 use_thy "WFrec";
 use_thy "Partial";