src/HOL/Complex/ROOT.ML

--- a/src/HOL/Complex/ROOT.ML	Tue May 06 12:29:49 2003 +0200
+++ b/src/HOL/Complex/ROOT.ML	Tue May 06 17:45:54 2003 +0200
@@ -5,5 +5,7 @@
 The Complex Numbers
 *)
 
+no_document time_use_thy "Ring_and_Field";
+with_path "../Real" use_thy "Real";
 with_path "../Hyperreal" use_thy "Hyperreal";
 time_use_thy "CLim";