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";