# HG changeset patch
# User wenzelm
# Date 1190906535 -7200
# Node ID 36750aca7a77c35bd45b888af8d7f0626fcac594
# Parent  e9f9d4297bda5e81d0352b1b23e2c7fa42d4da5b
some more simultaneous use_thys;

diff -r e9f9d4297bda -r 36750aca7a77 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Thu Sep 27 11:46:05 2007 +0200
+++ b/src/HOL/ex/ROOT.ML	Thu Sep 27 17:22:15 2007 +0200
@@ -6,7 +6,16 @@
 
 no_document use_thys [
   "Parity",
-  "GCD"
+  "GCD",
+  "Classpackage",
+  "Eval",
+  "State_Monad",
+  "Pretty_Int",
+  "Efficient_Nat",
+  "Codegenerator",
+  "Codegenerator_Pretty",
+  "FuncSet",
+  "Word"
 ];
 
 use_thys [
@@ -39,26 +48,16 @@
   "MT",
   "Unification",
   "Commutative_RingEx",
-  "Commutative_Ring_Complete"
+  "Commutative_Ring_Complete",
+  "Eval_Examples",
+  "Random",
+  "Primrec",
+  "Tarski",
+  "Adder"
 ];
 
-no_document time_use_thy "Classpackage";
-
-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 "Efficient_Nat";
-no_document time_use_thy "Codegenerator";
-no_document time_use_thy "Codegenerator_Pretty";
-
-
 setmp proofs 2 time_use_thy "Hilbert_Classical";
 
-time_use_thy "Primrec";
 time_use_thy "Classical";
 time_use_thy "set";
 
@@ -71,9 +70,6 @@
 
 time_use_thy "NBE";
 
-no_document use_thy "FuncSet";
-time_use_thy "Tarski";
-
 time_use_thy "SVC_Oracle";
 if_svc_enabled time_use_thy "svc_test";
 
@@ -91,8 +87,5 @@
 time_use_thy "Quickcheck_Examples";
 no_document time_use_thy "NormalForm";
 
-no_document use_thy "Word";
-time_use_thy "Adder";
-
 HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew";
 HTML.with_charset "utf-8" (no_document time_use_thy) "Chinese";