1.1 --- a/src/HOL/Complex/ROOT.ML	Sun Jul 22 23:23:39 2007 +0200
     1.2 +++ b/src/HOL/Complex/ROOT.ML	Sun Jul 22 23:33:57 2007 +0200
     1.3 @@ -5,9 +5,5 @@
     1.4  The Complex Numbers.
     1.5  *)
     1.6  
     1.7 -no_document use_thy "Infinite_Set";
     1.8 -no_document use_thy "Parity";
     1.9 -
    1.10 -with_path "../Real" use_thy "Float";
    1.11 -with_path "../Hyperreal" use_thy "Hyperreal";
    1.12 -use_thy "Complex_Main";
    1.13 +no_document use_thys ["Infinite_Set", "Parity"];
    1.14 +use_thys ["../Real/Float", "Complex_Main"];