src/HOL/Complex/Complex_Main.thy
changeset 28944 e27abf0db984
parent 28866 30cd9d89a0fb
equal deleted inserted replaced
28943:9fb44eb4425d 28944:e27abf0db984
     7 header{*Comprehensive Complex Theory*}
     7 header{*Comprehensive Complex Theory*}
     8 
     8 
     9 theory Complex_Main
     9 theory Complex_Main
    10 imports
    10 imports
    11   "../Main"
    11   "../Main"
       
    12   "../Real/ContNotDenum"
       
    13   "../Real/Real"
    12   Fundamental_Theorem_Algebra
    14   Fundamental_Theorem_Algebra
    13   "../Hyperreal/Log"
    15   "../Hyperreal/Log"
    14   "../Hyperreal/Ln"
    16   "../Hyperreal/Ln"
    15   "../Hyperreal/Taylor"
    17   "../Hyperreal/Taylor"
    16   "../Hyperreal/Integration"
    18   "../Hyperreal/Integration"