# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1672575840 0
# Node ID 04c7ec38874e8a8805cb690dcf3b3e9de8f70c88
# Parent  d908a7d3ed1b298234b84326dc5460e1fe01a7c0
removed an unfortunate sledgehammer command

diff -r d908a7d3ed1b -r 04c7ec38874e src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Sun Jan 01 01:43:02 2023 +0000
+++ b/src/HOL/Analysis/Function_Topology.thy	Sun Jan 01 12:24:00 2023 +0000
@@ -335,11 +335,8 @@
   "openin (product_topology X I) S \<longleftrightarrow>
     (\<forall>x \<in> S. \<exists>U. finite {i \<in> I. U i \<noteq> topspace(X i)} \<and>
                  (\<forall>i \<in> I. openin (X i) (U i)) \<and> x \<in> Pi\<^sub>E I U \<and> Pi\<^sub>E I U \<subseteq> S)"
-sledgehammer [isar_proofs, provers = "cvc4 z3 spass e vampire verit", timeout = 77]
   unfolding openin_product_topology arbitrary_union_of_alt product_topology_base_alt topspace_product_topology
-  apply safe
-  apply (drule bspec; blast)+
-  done
+  by (smt (verit, best))
 
 lemma closure_of_product_topology:
   "(product_topology X I) closure_of (PiE I S) = PiE I (\<lambda>i. (X i) closure_of (S i))"