# HG changeset patch
# User huffman
# Date 1158072244 -7200
# Node ID 3ef9eb57d769e7b92d2062bfac0e51c3df7e74e3
# Parent  5ede702cd2cabc7ba4f5f58fb8c00faf4aed65c2
remove extra dependency

diff -r 5ede702cd2ca -r 3ef9eb57d769 src/HOL/Hyperreal/NthRoot.thy
--- a/src/HOL/Hyperreal/NthRoot.thy	Tue Sep 12 14:50:11 2006 +0200
+++ b/src/HOL/Hyperreal/NthRoot.thy	Tue Sep 12 16:44:04 2006 +0200
@@ -7,7 +7,7 @@
 header{*Existence of Nth Root*}
 
 theory NthRoot
-imports SEQ HSeries
+imports SEQ
 begin
 
 text {*