# HG changeset patch
# User huffman
# Date 1179209431 -7200
# Node ID d95580341be5941088541b7d61928eb86414b5fb
# Parent  1cd8cc21a7c312894fd0e3b329a5a98e78e27b9e
minimize imports

diff -r 1cd8cc21a7c3 -r d95580341be5 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?*)