# HG changeset patch
# User huffman
# Date 1176419172 -7200
# Node ID 83878e551c8cbf40d5f7e528bed8a1360e708354
# Parent  c2b6b5a9e13607664968935cd10a5082413530cc
minimize imports

diff -r c2b6b5a9e136 -r 83878e551c8c src/HOL/Complex/Complex.thy
--- 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
diff -r c2b6b5a9e136 -r 83878e551c8c src/HOL/Complex/Complex_Main.thy
--- 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
diff -r c2b6b5a9e136 -r 83878e551c8c src/HOL/Complex/NSCA.thy
--- 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
diff -r c2b6b5a9e136 -r 83878e551c8c src/HOL/Complex/NSComplex.thy
--- 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"