# HG changeset patch
# User huffman
# Date 1179505239 -7200
# Node ID e6b5459f902897f7b2c915d4365ad4f01175f82a
# Parent  01c295dd4a36263c719280c5df24052f10662033
minimize imports

diff -r 01c295dd4a36 -r e6b5459f9028 src/HOL/Hyperreal/HLim.thy
--- a/src/HOL/Hyperreal/HLim.thy	Fri May 18 17:35:07 2007 +0200
+++ b/src/HOL/Hyperreal/HLim.thy	Fri May 18 18:20:39 2007 +0200
@@ -8,7 +8,7 @@
 header{* Limits and Continuity (Nonstandard) *}
 
 theory HLim
-imports HSEQ Lim
+imports Star Lim
 begin
 
 text{*Nonstandard Definitions*}