# HG changeset patch
# User wenzelm
# Date 1181076418 -7200
# Node ID 3f9ef4bf3f31030ed8e8d49b596ce2a26b0b6e67
# Parent  83924bdbcc189641e67ba8668196c31782e40f19
tuned document;
added Groebner_Examples;

diff -r 83924bdbcc18 -r 3f9ef4bf3f31 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Tue Jun 05 22:46:57 2007 +0200
+++ b/src/HOL/ex/ROOT.ML	Tue Jun 05 22:46:58 2007 +0200
@@ -8,9 +8,17 @@
 no_document use_thy "GCD";
 
 no_document time_use_thy "Classpackage";
-no_document time_use_thy "Eval_examples";
-no_document time_use_thy "Random";
-no_document time_use_thy "Codegenerator_Rat";
+
+no_document time_use_thy "Eval";
+time_use_thy "Eval_Examples";
+
+no_document time_use_thy "State_Monad";
+no_document time_use_thy "Pretty_Int";
+time_use_thy "Random";
+
+no_document time_use_thy "ExecutableRat";
+no_document time_use_thy "EfficientNat";
+time_use_thy "Codegenerator_Rat";
 no_document time_use_thy "Codegenerator";
 
 time_use_thy "Higher_Order_Logic";
@@ -49,6 +57,8 @@
 time_use_thy "Puzzle";
 
 time_use_thy "Lagrange";
+time_use_thy "Groebner_Examples";
+
 time_use_thy "Commutative_RingEx";
 time_use_thy "Commutative_Ring_Complete";
 time_use_thy "Reflection";