--- 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 {*