# HG changeset patch
# User wenzelm
# Date 1186752491 -7200
# Node ID 2e2d81b4f1849f45c23dfaaa9354da8cbd81f66a
# Parent  5458fbf18276366fc2ec8648fab222453eacba7e
simultaneous use_thys;

diff -r 5458fbf18276 -r 2e2d81b4f184 src/HOL/Complex/ex/ROOT.ML
--- a/src/HOL/Complex/ex/ROOT.ML	Fri Aug 10 15:13:18 2007 +0200
+++ b/src/HOL/Complex/ex/ROOT.ML	Fri Aug 10 15:28:11 2007 +0200
@@ -1,28 +1,28 @@
 (*  Title:      HOL/Complex/ex/ROOT.ML
     ID:         $Id$
 
-Miscellaneous examples involving the Reals, Hyperreals, etc.
+Miscellaneous examples.
 *)
 
-use_thy "BinEx";
-no_document (with_path "../../NumberTheory" use_thy) "Factorization";
-(*These two examples just need the theory Primes.*)
-use_thy "Sqrt";
-use_thy "Sqrt_Script";
-(*This example also needs the theory Factorization.*)
-use_thy "NSPrimes";
+no_document use_thys [
+  "../../NumberTheory/Factorization",
+  "BigO",
+  "NatPair"
+];
 
-no_document use_thy "BigO";
-use_thy "BigO_Complex";
+use_thys [
+  "BinEx",
+  "Sqrt",
+  "Sqrt_Script",
+  "NSPrimes",
+  "BigO_Complex",
 
-use_thy "Arithmetic_Series_Complex";
-use_thy "HarmonicSeries";
+  "Arithmetic_Series_Complex",
+  "HarmonicSeries",
 
-no_document use_thy "NatPair";
-use_thy "DenumRat";
+  "DenumRat"
+];
 
 if String.isPrefix "smlnj" ml_system then ()  (* FIXME tmp *)
-else use_thy "MIR";
+else use_thys ["MIR", "ReflectedFerrack"];
 
-if String.isPrefix "smlnj" ml_system then ()  (* FIXME tmp *)
-else use_thy "ReflectedFerrack";