changeset 22522 | 783c8dbe3ade |
parent 22505 | e2d378a97905 |
child 22528 | 8501c4a62a3c |
--- a/src/HOL/ex/ROOT.ML Mon Mar 26 14:53:04 2007 +0200 +++ b/src/HOL/ex/ROOT.ML Mon Mar 26 14:53:05 2007 +0200 @@ -8,7 +8,7 @@ no_document use_thy "GCD"; no_document time_use_thy "Classpackage"; -no_document time_use_thy "CodeEval"; +no_document time_use_thy "Eval_examples"; no_document time_use_thy "CodeRandom"; no_document time_use_thy "Codegenerator_Rat"; no_document time_use_thy "Codegenerator";