# HG changeset patch
# User hoelzl
# Date 1364296858 -3600
# Node ID d3d170a2887ff2a9344e797d074f6e5d25da840a
# Parent  7cb5ac44ca9e413d06ca628b7d7370b1a10521a1
HOL-NSA should only import Complex_Main

diff -r 7cb5ac44ca9e -r d3d170a2887f src/HOL/NSA/HDeriv.thy
--- 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*}
diff -r 7cb5ac44ca9e -r d3d170a2887f src/HOL/NSA/HLim.thy
--- 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*}
diff -r 7cb5ac44ca9e -r d3d170a2887f src/HOL/NSA/HLog.thy
--- 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
 
 
diff -r 7cb5ac44ca9e -r d3d170a2887f src/HOL/NSA/HSEQ.thy
--- 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
diff -r 7cb5ac44ca9e -r d3d170a2887f src/HOL/NSA/HSeries.thy
--- 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
diff -r 7cb5ac44ca9e -r d3d170a2887f src/HOL/NSA/HyperDef.thy
--- 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"
diff -r 7cb5ac44ca9e -r d3d170a2887f src/HOL/NSA/Hyperreal.thy
--- 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
diff -r 7cb5ac44ca9e -r d3d170a2887f src/HOL/NSA/NSComplex.thy
--- 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"