Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
changeset 62843 313d3b697c9a
parent 62375 670063003ad3 
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Mon Apr 04 09:45:04 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Mon Apr 04 16:52:56 2016 +0100
@@ -23,7 +23,7 @@
 lemma compact_eq_closed:
   fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set"
   shows "compact S \<longleftrightarrow> closed S"
-  using closed_inter_compact[of S, OF _ compact_UNIV] compact_imp_closed
+  using closed_Int_compact[of S, OF _ compact_UNIV] compact_imp_closed
   by auto
 
 lemma closed_contains_Sup_cl:
isabelle