removed nonstandard analysis theories to HOL-NSA
authorhuffman
Thu, 03 Jul 2008 17:58:10 +0200
changeset 27472 47bc28e011d5
parent 27471 f7aa166d9559
child 27473 83f973424116
removed nonstandard analysis theories to HOL-NSA
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