# HG changeset patch
# User wenzelm
# Date 1185140037 -7200
# Node ID 0f8ad104452725937b5b7f1ae4d9a2fc7093a9f3
# Parent  fcbee3512a995523119dc73cd14413f2afdbd204
simultaneous use_thys;

diff -r fcbee3512a99 -r 0f8ad1044527 src/HOL/Complex/ROOT.ML
--- a/src/HOL/Complex/ROOT.ML	Sun Jul 22 23:23:39 2007 +0200
+++ b/src/HOL/Complex/ROOT.ML	Sun Jul 22 23:33:57 2007 +0200
@@ -5,9 +5,5 @@
 The Complex Numbers.
 *)
 
-no_document use_thy "Infinite_Set";
-no_document use_thy "Parity";
-
-with_path "../Real" use_thy "Float";
-with_path "../Hyperreal" use_thy "Hyperreal";
-use_thy "Complex_Main";
+no_document use_thys ["Infinite_Set", "Parity"];
+use_thys ["../Real/Float", "Complex_Main"];