HOL-NSA should only import Complex_Main

--- a/src/HOL/NSA/HDeriv.thy	Tue Mar 26 12:20:57 2013 +0100
+++ b/src/HOL/NSA/HDeriv.thy	Tue Mar 26 12:20:58 2013 +0100
@@ -7,7 +7,7 @@
 header{* Differentiation (Nonstandard) *}
 
 theory HDeriv
-imports Deriv HLim
+imports HLim
 begin
 
 text{*Nonstandard Definitions*}

--- a/src/HOL/NSA/HLim.thy	Tue Mar 26 12:20:57 2013 +0100
+++ b/src/HOL/NSA/HLim.thy	Tue Mar 26 12:20:58 2013 +0100
@@ -6,7 +6,7 @@
 header{* Limits and Continuity (Nonstandard) *}
 
 theory HLim
-imports Star Lim
+imports Star
 begin
 
 text{*Nonstandard Definitions*}

--- a/src/HOL/NSA/HLog.thy	Tue Mar 26 12:20:57 2013 +0100
+++ b/src/HOL/NSA/HLog.thy	Tue Mar 26 12:20:58 2013 +0100
@@ -6,7 +6,7 @@
 header{*Logarithms: Non-Standard Version*}
 
 theory HLog
-imports Log HTranscendental
+imports HTranscendental
 begin
 
 

--- a/src/HOL/NSA/HSEQ.thy	Tue Mar 26 12:20:57 2013 +0100
+++ b/src/HOL/NSA/HSEQ.thy	Tue Mar 26 12:20:58 2013 +0100
@@ -9,7 +9,7 @@
 header {* Sequences and Convergence (Nonstandard) *}
 
 theory HSEQ
-imports SEQ NatStar
+imports Limits NatStar
 begin
 
 definition

--- a/src/HOL/NSA/HSeries.thy	Tue Mar 26 12:20:57 2013 +0100
+++ b/src/HOL/NSA/HSeries.thy	Tue Mar 26 12:20:58 2013 +0100
@@ -8,7 +8,7 @@
 header{*Finite Summation and Infinite Series for Hyperreals*}
 
 theory HSeries
-imports Series HSEQ
+imports HSEQ
 begin
 
 definition

--- a/src/HOL/NSA/HyperDef.thy	Tue Mar 26 12:20:57 2013 +0100
+++ b/src/HOL/NSA/HyperDef.thy	Tue Mar 26 12:20:58 2013 +0100
@@ -7,7 +7,7 @@
 header{*Construction of Hyperreals Using Ultrafilters*}
 
 theory HyperDef
-imports HyperNat Real
+imports Complex_Main HyperNat
 begin
 
 type_synonym hypreal = "real star"

--- a/src/HOL/NSA/Hyperreal.thy	Tue Mar 26 12:20:57 2013 +0100
+++ b/src/HOL/NSA/Hyperreal.thy	Tue Mar 26 12:20:58 2013 +0100
@@ -7,7 +7,7 @@
 *)
 
 theory Hyperreal
-imports Ln Deriv Taylor HLog
+imports HLog
 begin
 
 end

--- a/src/HOL/NSA/NSComplex.thy	Tue Mar 26 12:20:57 2013 +0100
+++ b/src/HOL/NSA/NSComplex.thy	Tue Mar 26 12:20:58 2013 +0100
@@ -6,7 +6,7 @@
 header{*Nonstandard Complex Numbers*}
 
 theory NSComplex
-imports Complex NSA
+imports NSA
 begin
 
 type_synonym hcomplex = "complex star"