src/HOL/ex/ROOT.ML
changeset 20436 0af8655ab0bb
parent 20427 0b102b4182de
child 20597 65fe827aa595
     1.1 --- a/src/HOL/ex/ROOT.ML	Wed Aug 30 08:30:09 2006 +0200
     1.2 +++ b/src/HOL/ex/ROOT.ML	Wed Aug 30 08:34:45 2006 +0200
     1.3 @@ -7,6 +7,7 @@
     1.4  no_document time_use_thy "Classpackage";
     1.5  no_document time_use_thy "Codegenerator";
     1.6  no_document time_use_thy "CodeOperationalEquality";
     1.7 +no_document time_use_thy "CodeCollections";
     1.8  no_document time_use_thy "CodeEval";
     1.9  no_document time_use_thy "CodeRandom";
    1.10