# HG changeset patch
# User huffman
# Date 1273552428 25200
# Node ID 38a480e0346f9e9a3c5a2844ef4a5377bd298a28
# Parent  9207505d1ee563e03169368e24b4265fd90f9df0
minimize imports

diff -r 9207505d1ee5 -r 38a480e0346f src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon May 10 21:27:52 2010 -0700
+++ b/src/HOL/Limits.thy	Mon May 10 21:33:48 2010 -0700
@@ -5,7 +5,7 @@
 header {* Filters and Limits *}
 
 theory Limits
-imports RealVector RComplete
+imports RealVector
 begin
 
 subsection {* Nets *}
diff -r 9207505d1ee5 -r 38a480e0346f src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Mon May 10 21:27:52 2010 -0700
+++ b/src/HOL/SEQ.thy	Mon May 10 21:33:48 2010 -0700
@@ -10,7 +10,7 @@
 header {* Sequences and Convergence *}
 
 theory SEQ
-imports Limits
+imports Limits RComplete
 begin
 
 abbreviation