# HG changeset patch
# User huffman
# Date 1179349425 -7200
# Node ID 3314057c3b575aa1e1adb03863da32ecc1c4e898
# Parent  bff3fcdeecd38c3ffd0351239d94eb39902a2474
minimize imports

diff -r bff3fcdeecd3 -r 3314057c3b57 src/HOL/Complex/Complex_Main.thy
--- a/src/HOL/Complex/Complex_Main.thy	Wed May 16 09:45:22 2007 +0200
+++ b/src/HOL/Complex/Complex_Main.thy	Wed May 16 23:03:45 2007 +0200
@@ -7,7 +7,7 @@
 header{*Comprehensive Complex Theory*}
 
 theory Complex_Main
-imports CLim "../Hyperreal/HLog"
+imports CLim "../Hyperreal/Hyperreal"
 begin
 
 end
diff -r bff3fcdeecd3 -r 3314057c3b57 src/HOL/Hyperreal/HTranscendental.thy
--- a/src/HOL/Hyperreal/HTranscendental.thy	Wed May 16 09:45:22 2007 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy	Wed May 16 23:03:45 2007 +0200
@@ -8,7 +8,7 @@
 header{*Nonstandard Extensions of Transcendental Functions*}
 
 theory HTranscendental
-imports Transcendental Integration HSeries HDeriv
+imports Transcendental HSeries HDeriv
 begin
 
 definition
diff -r bff3fcdeecd3 -r 3314057c3b57 src/HOL/Hyperreal/Hyperreal.thy
--- a/src/HOL/Hyperreal/Hyperreal.thy	Wed May 16 09:45:22 2007 +0200
+++ b/src/HOL/Hyperreal/Hyperreal.thy	Wed May 16 23:03:45 2007 +0200
@@ -8,7 +8,7 @@
 *)
 
 theory Hyperreal
-imports Poly Taylor HLog
+imports Ln Poly Taylor Integration HLog
 begin
 
 end
diff -r bff3fcdeecd3 -r 3314057c3b57 src/HOL/Hyperreal/MacLaurin.thy
--- a/src/HOL/Hyperreal/MacLaurin.thy	Wed May 16 09:45:22 2007 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Wed May 16 23:03:45 2007 +0200
@@ -7,7 +7,7 @@
 header{*MacLaurin Series*}
 
 theory MacLaurin
-imports Log
+imports Transcendental
 begin
 
 subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*}
diff -r bff3fcdeecd3 -r 3314057c3b57 src/HOL/Hyperreal/Poly.thy
--- a/src/HOL/Hyperreal/Poly.thy	Wed May 16 09:45:22 2007 +0200
+++ b/src/HOL/Hyperreal/Poly.thy	Wed May 16 23:03:45 2007 +0200
@@ -9,7 +9,7 @@
 header{*Univariate Real Polynomials*}
 
 theory Poly
-imports Ln
+imports Transcendental
 begin
 
 text{*Application of polynomial as a real function.*}