# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# 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 \<open>convex U\<close> open_ball]
     by (fastforce simp add: Int_commute)
   have "rel_frontier S homeomorphic rel_frontier (ball z 1 \<inter> U)"
-    apply (rule homeomorphic_rel_frontiers_convex_bounded_sets)
-    apply (auto simp: \<open>affine U\<close> affine_imp_convex convex_Int affdS assms)
-    done
+    by (rule homeomorphic_rel_frontiers_convex_bounded_sets)
+       (auto simp: \<open>affine U\<close> affine_imp_convex convex_Int affdS assms)
   also have "... = sphere z 1 \<inter> U"
     using convex_affine_rel_frontier_Int [of "ball z 1" U]
     by (simp add: \<open>affine U\<close> 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 \<open>affine T\<close> \<open>affine U\<close> \<open>z \<in> U\<close>)
+    by (rule homeomorphic_punctured_affine_sphere_affine)
+       (use a him in \<open>auto simp: affS affdS \<open>affine T\<close> \<open>affine U\<close> \<open>z \<in> U\<close>\<close>)
   finally show ?thesis .
 qed