--- a/src/HOL/Hyperreal/HTranscendental.thy Sun Sep 24 04:00:03 2006 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy Sun Sep 24 04:00:46 2006 +0200
@@ -8,7 +8,7 @@
header{*Nonstandard Extensions of Transcendental Functions*}
theory HTranscendental
-imports Transcendental Integration
+imports Transcendental Integration HSeries
begin
text{*really belongs in Transcendental*}
--- a/src/HOL/Hyperreal/Transcendental.thy Sun Sep 24 04:00:03 2006 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy Sun Sep 24 04:00:46 2006 +0200
@@ -8,7 +8,7 @@
header{*Power Series, Transcendental Functions etc.*}
theory Transcendental
-imports NthRoot Fact HSeries EvenOdd Lim
+imports NthRoot Fact Series EvenOdd Lim
begin
definition