src/HOL/ex/ROOT.ML
changeset 20427 0b102b4182de
parent 20400 0ad2f3bbd4f0
child 20436 0af8655ab0bb
--- a/src/HOL/ex/ROOT.ML	Tue Aug 29 14:31:13 2006 +0200
+++ b/src/HOL/ex/ROOT.ML	Tue Aug 29 14:31:14 2006 +0200
@@ -6,9 +6,9 @@
 
 no_document time_use_thy "Classpackage";
 no_document time_use_thy "Codegenerator";
-no_document time_use_thy "CodeEmbed";
+no_document time_use_thy "CodeOperationalEquality";
+no_document time_use_thy "CodeEval";
 no_document time_use_thy "CodeRandom";
-no_document time_use_thy "CodeRevappl";
 
 time_use_thy "Higher_Order_Logic";
 time_use_thy "Abstract_NAT";