# HG changeset patch
# User huffman
# Date 1228174608 28800
# Node ID e27abf0db98478cde433a96eb1c9b31a3b1e8c43
# Parent  9fb44eb4425dd5f73c65e456c6459e20ee459fe3
clean up imports related to ContNotDenum

diff -r 9fb44eb4425d -r e27abf0db984 src/HOL/Complex/Complex.thy
--- 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
diff -r 9fb44eb4425d -r e27abf0db984 src/HOL/Complex/Complex_Main.thy
--- 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"
diff -r 9fb44eb4425d -r e27abf0db984 src/HOL/Hyperreal/Fact.thy
--- 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"
diff -r 9fb44eb4425d -r e27abf0db984 src/HOL/Hyperreal/SEQ.thy
--- 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