# HG changeset patch
# User huffman
# Date 1215100690 -7200
# Node ID 47bc28e011d5207702a32b26186c95136f36c12d
# Parent  f7aa166d9559e4ea85ac33340bc19ac0257bf968
removed nonstandard analysis theories to HOL-NSA

diff -r f7aa166d9559 -r 47bc28e011d5 src/HOL/Complex/Complex_Main.thy
--- a/src/HOL/Complex/Complex_Main.thy	Thu Jul 03 17:57:01 2008 +0200
+++ b/src/HOL/Complex/Complex_Main.thy	Thu Jul 03 17:58:10 2008 +0200
@@ -7,7 +7,13 @@
 header{*Comprehensive Complex Theory*}
 
 theory Complex_Main
-imports Main Fundamental_Theorem_Algebra CLim "../Hyperreal/Hyperreal"
+imports
+  Main
+  Fundamental_Theorem_Algebra
+  "../Hyperreal/Log"
+  "../Hyperreal/Ln"
+  "../Hyperreal/Taylor"
+  "../Hyperreal/Integration"
 begin
 
 end