src/HOL/ex/ROOT.ML
changeset 22505 e2d378a97905
parent 22167 c3afded569ea
child 22522 783c8dbe3ade
--- a/src/HOL/ex/ROOT.ML	Fri Mar 23 09:40:45 2007 +0100
+++ b/src/HOL/ex/ROOT.ML	Fri Mar 23 09:40:47 2007 +0100
@@ -8,7 +8,6 @@
 no_document use_thy "GCD";
 
 no_document time_use_thy "Classpackage";
-no_document time_use_thy "CodeCollections";
 no_document time_use_thy "CodeEval";
 no_document time_use_thy "CodeRandom";
 no_document time_use_thy "Codegenerator_Rat";