author | huffman |
Thu, 03 Jul 2008 17:58:10 +0200 | |
changeset 27472 | 47bc28e011d5 |
parent 27471 | f7aa166d9559 |
child 27473 | 83f973424116 |
--- a/src/HOL/Complex/Complex_Main.thy Thu Jul 03 17:57:01 2008 +0200 +++ b/src/HOL/Complex/Complex_Main.thy Thu Jul 03 17:58:10 2008 +0200 @@ -7,7 +7,13 @@ header{*Comprehensive Complex Theory*} theory Complex_Main -imports Main Fundamental_Theorem_Algebra CLim "../Hyperreal/Hyperreal" +imports + Main + Fundamental_Theorem_Algebra + "../Hyperreal/Log" + "../Hyperreal/Ln" + "../Hyperreal/Taylor" + "../Hyperreal/Integration" begin end