# HG changeset patch # User paulson # 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 \ S" "y \ S" - obtains g where "polynomial_function g" "path_image g \ S" "pathstart g = x" "pathfinish g = y" + shows "\g. polynomial_function g \ path_image g \ S \ pathstart g = x \ 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: "\t. t \ {0..1} \ norm(pf t - p t) < e" using path_approx_polynomial_function [OF \path p\ \0 < e\] by blast - show thesis - proof + show ?thesis + proof (intro exI conjI) show "polynomial_function pf" by fact show "pathstart pf = x" "pathfinish pf = y"