# HG changeset patch
# User immler
# Date 1463774499 -7200
# Node ID 2394b0db133ffb2bdc3a730a3c63473578576818
# Parent  71059cf60658458955a901d7b050411c35486502
removed smt proof

diff -r 71059cf60658 -r 2394b0db133f src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri May 20 07:54:54 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri May 20 22:01:39 2016 +0200
@@ -5976,17 +5976,15 @@
   thus "isCont ((indicator A)::'a \<Rightarrow> real) x"
   proof
     assume int: "x \<in> interior A"
-    hence "\<exists>U. open U \<and> x \<in> U \<and> U \<subseteq> A" unfolding interior_def by auto
-    then guess U .. note U = this
+    then obtain U where U: "open U" "x \<in> U" "U \<subseteq> A" unfolding interior_def by auto
     hence "\<forall>y\<in>U. indicator A y = (1::real)" unfolding indicator_def by auto
     hence "continuous_on U (indicator A)" by (simp add: continuous_on_const indicator_eq_1_iff)
     thus ?thesis using U continuous_on_eq_continuous_at by auto
   next
     assume ext: "x \<in> interior (-A)"
-    hence "\<exists>U. open U \<and> x \<in> U \<and> U \<subseteq> -A" unfolding interior_def by auto
-    then guess U .. note U = this
-    hence "\<forall>y\<in>U. indicator A y = (0::real)" unfolding indicator_def by auto
-    hence "continuous_on U (indicator A)" by (smt U continuous_on_topological indicator_def)
+    then obtain U where U: "open U" "x \<in> U" "U \<subseteq> -A" unfolding interior_def by auto
+    then have "continuous_on U (indicator A)"
+      using continuous_on_topological by (auto simp: subset_iff)
     thus ?thesis using U continuous_on_eq_continuous_at by auto
   qed
 qed