changeset 16784 | 92ff7c903585 |
parent 14334 | 6137d24eef79 |
child 20809 | 6c4fd0b4b63a |
--- a/src/HOL/Complex/ROOT.ML Tue Jul 12 23:42:11 2005 +0200 +++ b/src/HOL/Complex/ROOT.ML Wed Jul 13 09:53:50 2005 +0200 @@ -5,6 +5,6 @@ The Complex Numbers *) -with_path "../Real" use_thy "Real"; +with_path "../Real" use_thy "Float"; with_path "../Hyperreal" use_thy "Hyperreal"; time_use_thy "Complex_Main";