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";