changeset 28944 | e27abf0db984 |
parent 26311 | 81a0fc28b0de |
--- a/src/HOL/Complex/Complex.thy Mon Dec 01 22:00:38 2008 +0100 +++ b/src/HOL/Complex/Complex.thy Mon Dec 01 15:36:48 2008 -0800 @@ -8,7 +8,7 @@ header {* Complex Numbers: Rectangular and Polar Representations *} theory Complex -imports "../Real/Real" "../Hyperreal/Transcendental" +imports "../Hyperreal/Transcendental" begin datatype complex = Complex real real