src/HOL/ex/ROOT.ML
changeset 22067 39d5d42116c4
parent 21911 e29bcab0c81c
child 22140 0d49078c28bd
     1.1 --- a/src/HOL/ex/ROOT.ML	Tue Jan 16 08:06:52 2007 +0100
     1.2 +++ b/src/HOL/ex/ROOT.ML	Tue Jan 16 08:06:55 2007 +0100
     1.3 @@ -11,6 +11,7 @@
     1.4  no_document time_use_thy "CodeCollections";
     1.5  no_document time_use_thy "CodeEval";
     1.6  no_document time_use_thy "CodeRandom";
     1.7 +no_document time_use_thy "Codegenerator_Rat";
     1.8  no_document time_use_thy "Codegenerator";
     1.9  
    1.10  time_use_thy "Higher_Order_Logic";