Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
minimize imports
authorhuffman
Mon, 10 May 2010 21:33:48 -0700
changeset 36822 38a480e0346f
parent 36821 9207505d1ee5
child 36823 001d1aad99de
minimize imports
src/HOL/Limits.thy file | annotate | diff | comparison | revisions
src/HOL/SEQ.thy file | annotate | diff | comparison | revisions 
--- 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 *}
--- 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
isabelle