# HG changeset patch # User paulson # Date 1524150606 -3600 # Node ID a1a023f08c8ffece4422f5121e7d34a35b3c6292 # Parent bb3e72f94adda9ea39f4979be5c9d1bc4bc7b40a tuning of a proof diff -r bb3e72f94add -r a1a023f08c8f src/HOL/Analysis/Homeomorphism.thy --- a/src/HOL/Analysis/Homeomorphism.thy Thu Apr 19 14:49:19 2018 +0100 +++ b/src/HOL/Analysis/Homeomorphism.thy Thu Apr 19 16:10:06 2018 +0100 @@ -881,9 +881,8 @@ using aff_dim_convex_Int_open [OF \convex U\ open_ball] by (fastforce simp add: Int_commute) have "rel_frontier S homeomorphic rel_frontier (ball z 1 \ U)" - apply (rule homeomorphic_rel_frontiers_convex_bounded_sets) - apply (auto simp: \affine U\ affine_imp_convex convex_Int affdS assms) - done + by (rule homeomorphic_rel_frontiers_convex_bounded_sets) + (auto simp: \affine U\ affine_imp_convex convex_Int affdS assms) also have "... = sphere z 1 \ U" using convex_affine_rel_frontier_Int [of "ball z 1" U] by (simp add: \affine U\ bne) @@ -903,9 +902,8 @@ by (force simp: h [symmetric] image_comp o_def kh) qed (auto intro: continuous_on_subset hcon kcon simp: kh hk) also have "... homeomorphic T" - apply (rule homeomorphic_punctured_affine_sphere_affine) - using a him - by (auto simp: affS affdS \affine T\ \affine U\ \z \ U\) + by (rule homeomorphic_punctured_affine_sphere_affine) + (use a him in \auto simp: affS affdS \affine T\ \affine U\ \z \ U\\) finally show ?thesis . qed