# HG changeset patch
# User huffman
# Date 1159063246 -7200
# Node ID 136b206327a4b3135a3779c015a72769dbb4aeb2
# Parent  4950e45442b8907ce071f65301f0bbcb17594bb9
remove extra dependencies

diff -r 4950e45442b8 -r 136b206327a4 src/HOL/Hyperreal/HTranscendental.thy
--- 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*}
diff -r 4950e45442b8 -r 136b206327a4 src/HOL/Hyperreal/Transcendental.thy
--- 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