minimize imports
authorhuffman
Tue, 15 May 2007 08:10:31 +0200
changeset 22979 d95580341be5
parent 22978 1cd8cc21a7c3
child 22980 1226d861eefb
minimize imports
src/HOL/Complex/CLim.thy
--- a/src/HOL/Complex/CLim.thy	Tue May 15 07:28:08 2007 +0200
+++ b/src/HOL/Complex/CLim.thy	Tue May 15 08:10:31 2007 +0200
@@ -7,7 +7,7 @@
 header{*Limits, Continuity and Differentiation for Complex Functions*}
 
 theory CLim
-imports CSeries
+imports CStar
 begin
 
 (*not in simpset?*)