--- 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
--- a/src/HOL/Complex/Complex_Main.thy Mon Dec 01 22:00:38 2008 +0100
+++ b/src/HOL/Complex/Complex_Main.thy Mon Dec 01 15:36:48 2008 -0800
@@ -9,6 +9,8 @@
theory Complex_Main
imports
"../Main"
+ "../Real/ContNotDenum"
+ "../Real/Real"
Fundamental_Theorem_Algebra
"../Hyperreal/Log"
"../Hyperreal/Ln"
--- a/src/HOL/Hyperreal/Fact.thy Mon Dec 01 22:00:38 2008 +0100
+++ b/src/HOL/Hyperreal/Fact.thy Mon Dec 01 15:36:48 2008 -0800
@@ -7,7 +7,7 @@
header{*Factorial Function*}
theory Fact
-imports "../Real/Real"
+imports "../Real/RealDef"
begin
consts fact :: "nat => nat"
--- a/src/HOL/Hyperreal/SEQ.thy Mon Dec 01 22:00:38 2008 +0100
+++ b/src/HOL/Hyperreal/SEQ.thy Mon Dec 01 15:36:48 2008 -0800
@@ -9,7 +9,7 @@
header {* Sequences and Convergence *}
theory SEQ
-imports "../Real/Real" "../Real/ContNotDenum"
+imports "../Real/RealVector" "../Real/RComplete"
begin
definition