src/HOL/Complex.thy
changeset 58889 5b7a9633cfa8
parent 58740 cb9d84d3e7f2
child 59000 6eb0725503fc
equal deleted inserted replaced
58888:9537bf1c4853 58889:5b7a9633cfa8
     2     Author:      Jacques D. Fleuriot
     2     Author:      Jacques D. Fleuriot
     3     Copyright:   2001 University of Edinburgh
     3     Copyright:   2001 University of Edinburgh
     4     Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
     4     Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
     5 *)
     5 *)
     6 
     6 
     7 header {* Complex Numbers: Rectangular and Polar Representations *}
     7 section {* Complex Numbers: Rectangular and Polar Representations *}
     8 
     8 
     9 theory Complex
     9 theory Complex
    10 imports Transcendental
    10 imports Transcendental
    11 begin
    11 begin
    12 
    12