src/HOL/ex/ROOT.ML
changeset 20597 65fe827aa595
parent 20436 0af8655ab0bb
child 20812 cc6b31c2b9a2
     1.1 --- a/src/HOL/ex/ROOT.ML	Tue Sep 19 15:22:03 2006 +0200
     1.2 +++ b/src/HOL/ex/ROOT.ML	Tue Sep 19 15:22:05 2006 +0200
     1.3 @@ -6,7 +6,6 @@
     1.4  
     1.5  no_document time_use_thy "Classpackage";
     1.6  no_document time_use_thy "Codegenerator";
     1.7 -no_document time_use_thy "CodeOperationalEquality";
     1.8  no_document time_use_thy "CodeCollections";
     1.9  no_document time_use_thy "CodeEval";
    1.10  no_document time_use_thy "CodeRandom";