--- a/src/HOL/ex/ROOT.ML Thu Apr 13 12:01:15 2006 +0200
+++ b/src/HOL/ex/ROOT.ML Thu Apr 13 12:01:16 2006 +0200
@@ -4,6 +4,9 @@
Miscellaneous examples for Higher-Order Logic.
*)
+no_document time_use_thy "Classpackage";
+no_document time_use_thy "Codegenerator";
+
time_use_thy "Higher_Order_Logic";
time_use_thy "Abstract_NAT";
@@ -57,8 +60,6 @@
time_use_thy "Refute_Examples";
time_use_thy "Quickcheck_Examples";
-no_document time_use_thy "Classpackage";
-no_document time_use_thy "Codegenerator";
no_document time_use_thy "nbe";
no_document use_thy "Word";