# HG changeset patch
# User paulson
# Date 1572727944 0
# Node ID 7f1241a2bf300e0e59073a5ca87326e08cf8b292
# Parent  699ff83813c0b17f963d8f2b2a8b10a457b417c5# Parent  b86d307078377e01382e068135448d7e88f46174
merged

diff -r 699ff83813c0 -r 7f1241a2bf30 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Sat Nov 02 20:56:22 2019 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Sat Nov 02 20:52:24 2019 +0000
@@ -3162,14 +3162,8 @@
     assume "z \<in> ?lhs"
     have *: "z = (fst z, snd z)"
       by auto
-    have "z \<in> ?rhs"
-      using rel_interior_convex_cone_aux[of S "fst z" "snd z"] assms \<open>z \<in> ?lhs\<close>
-      apply auto
-      apply (rule_tac x = "fst z" in exI)
-      apply (rule_tac x = x in exI)
-      using *
-      apply auto
-      done
+    then have "z \<in> ?rhs"
+      using rel_interior_convex_cone_aux[of S "fst z" "snd z"] assms \<open>z \<in> ?lhs\<close> by fastforce
   }
   moreover
   {