src/HOL/Complex/ROOT.ML
changeset 13984 e055ba9020eb
parent 13966 2160abf7cfe7
child 14265 95b42e69436c
--- a/src/HOL/Complex/ROOT.ML	Thu May 08 15:23:21 2003 +0200
+++ b/src/HOL/Complex/ROOT.ML	Thu May 08 17:44:38 2003 +0200
@@ -8,4 +8,4 @@
 no_document time_use_thy "Ring_and_Field";
 with_path "../Real" use_thy "Real";
 with_path "../Hyperreal" use_thy "Hyperreal";
-time_use_thy "CLim";
+time_use_thy "Complex_Main";