# HG changeset patch
# User wenzelm
# Date 1231276122 -3600
# Node ID e6439dbfeee1dc6b24a06ee7d16cd1403a88190d
# Parent  2071939cf0fc6a21aecbabbf0f76d9b4cd0e4f9f
more parallel loading;

diff -r 2071939cf0fc -r e6439dbfeee1 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Tue Jan 06 21:55:51 2009 +0100
+++ b/src/HOL/ex/ROOT.ML	Tue Jan 06 22:08:42 2009 +0100
@@ -14,7 +14,9 @@
   "Term_Of_Syntax",
   "Codegenerator",
   "Codegenerator_Pretty",
-  "NormalForm"
+  "NormalForm",
+  "../NumberTheory/Factorization",
+  "../Library/BigO"
 ];
 
 use_thys [
@@ -62,7 +64,17 @@
   "PresburgerEx",
   "Reflected_Presburger",
   "Reflection",
-  "ReflectionEx"
+  "ReflectionEx",
+  "BinEx",
+  "Sqrt",
+  "Sqrt_Script",
+  "BigO_Complex",
+  "Arithmetic_Series_Complex",
+  "HarmonicSeries",
+  "MIR",
+  "ReflectedFerrack",
+  "Refute_Examples",
+  "Quickcheck_Examples"
 ];
 
 setmp Proofterm.proofs 2 use_thy "Hilbert_Classical";
@@ -73,7 +85,7 @@
 fun svc_enabled () = getenv "SVC_HOME" <> "";
 fun if_svc_enabled f x = if svc_enabled () then f x else ();
 
-if_svc_enabled time_use_thy "svc_test";
+if_svc_enabled use_thy "svc_test";
 
 
 (* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)
@@ -86,26 +98,4 @@
   use_thy "Sudoku"
 else ();
 
-time_use_thy "Refute_Examples";
-time_use_thy "Quickcheck_Examples";
-
 HTML.with_charset "utf-8" (no_document use_thys) ["Hebrew", "Chinese"];
-
-no_document use_thys [
-  "../NumberTheory/Factorization",
-  "../Library/BigO"
-];
-
-use_thys [
-  "BinEx",
-  "Sqrt",
-  "Sqrt_Script",
-  "BigO_Complex",
-
-  "Arithmetic_Series_Complex",
-  "HarmonicSeries",
-
-  "MIR",
-  "ReflectedFerrack"
-];
-