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/Abstract_Topology.thy
changeset 75455 91c16c5ad3e9
parent 75449 51e05af57455
child 77234 61fba09a3456 
--- a/src/HOL/Analysis/Abstract_Topology.thy	Wed May 11 10:42:24 2022 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Tue May 17 14:10:14 2022 +0100
@@ -3924,7 +3924,7 @@
       using \<open>(x, y) \<in> E1 \<times> E2\<close> \<open>x \<in> S\<close> \<open>y \<in> T\<close> by auto
     show "(E1 \<inter> S) \<times> (E2 \<inter> T) \<subseteq> U"
       using \<open>E1 \<times> E2 \<subseteq> E\<close> \<open>U = _\<close>
-      by (auto simp: )
+      by auto
   qed
 qed
isabelle