--- 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
--- 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
--- 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
--- 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*}
--- 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.*}