--- a/src/HOL/Complex/Complex.thy Fri Apr 13 00:48:12 2007 +0200
+++ b/src/HOL/Complex/Complex.thy Fri Apr 13 01:06:12 2007 +0200
@@ -8,7 +8,7 @@
header {* Complex Numbers: Rectangular and Polar Representations *}
theory Complex
-imports "../Hyperreal/HLog"
+imports "../Hyperreal/Transcendental"
begin
datatype complex = Complex real real
--- a/src/HOL/Complex/Complex_Main.thy Fri Apr 13 00:48:12 2007 +0200
+++ b/src/HOL/Complex/Complex_Main.thy Fri Apr 13 01:06:12 2007 +0200
@@ -7,7 +7,7 @@
header{*Comprehensive Complex Theory*}
theory Complex_Main
-imports CLim
+imports CLim "../Hyperreal/HLog"
begin
end
--- a/src/HOL/Complex/NSCA.thy Fri Apr 13 00:48:12 2007 +0200
+++ b/src/HOL/Complex/NSCA.thy Fri Apr 13 01:06:12 2007 +0200
@@ -6,7 +6,7 @@
header{*Non-Standard Complex Analysis*}
theory NSCA
-imports NSComplex
+imports NSComplex "../Hyperreal/HTranscendental"
begin
abbreviation
--- a/src/HOL/Complex/NSComplex.thy Fri Apr 13 00:48:12 2007 +0200
+++ b/src/HOL/Complex/NSComplex.thy Fri Apr 13 01:06:12 2007 +0200
@@ -8,7 +8,7 @@
header{*Nonstandard Complex Numbers*}
theory NSComplex
-imports Complex
+imports Complex "../Hyperreal/NSA"
begin
types hcomplex = "complex star"