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/Analysis/Path_Connected.thy
changeset 68120 2f161c6910f7
parent 68096 e58c9ac761cb
child 68296 69d680e94961 
--- a/src/HOL/Analysis/Path_Connected.thy	Sun May 06 23:59:14 2018 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Tue May 08 10:32:07 2018 +0100
@@ -6981,7 +6981,7 @@
     shows "S = {}"
 proof -
   obtain a b where "S \<subseteq> box a b"
-    by (meson assms bounded_subset_open_interval)
+    by (meson assms bounded_subset_box_symmetric)
   then have "a \<notin> S" "b \<notin> S"
     by auto
   then have "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> - S"
isabelle