# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1601919975 -3600
# Node ID becf08cb81e1246f8267203cf38246ba692940c2
# Parent  504fe736582099d7137f4d836c6defd6c6ffdbe7
reversion to the explicit existential quantifier

diff -r 504fe7365820 -r becf08cb81e1 src/HOL/Analysis/Weierstrass_Theorems.thy
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Mon Oct 05 12:47:19 2020 +0100
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Mon Oct 05 18:46:15 2020 +0100
@@ -1198,7 +1198,7 @@
   fixes S :: "'a::euclidean_space set"
   assumes S: "open S" "connected S"
       and "x \<in> S" "y \<in> S"
-    obtains g where "polynomial_function g" "path_image g \<subseteq> S" "pathstart g = x" "pathfinish g = y"
+    shows "\<exists>g. polynomial_function g \<and> path_image g \<subseteq> S \<and> pathstart g = x \<and> pathfinish g = y"
 proof -
   have "path_connected S" using assms
     by (simp add: connected_open_path_connected)
@@ -1224,8 +1224,8 @@
   obtain pf where "polynomial_function pf" and pf: "pathstart pf = pathstart p" "pathfinish pf = pathfinish p"
                    and pf_e: "\<And>t. t \<in> {0..1} \<Longrightarrow> norm(pf t - p t) < e"
     using path_approx_polynomial_function [OF \<open>path p\<close> \<open>0 < e\<close>] by blast
-  show thesis 
-  proof
+  show ?thesis 
+  proof (intro exI conjI)
     show "polynomial_function pf"
       by fact
     show "pathstart pf = x" "pathfinish pf = y"