src/HOL/Analysis/Homeomorphism.thy

       qed
     qed
   qed
 qed
 
-proposition (*FIXME needs name *)
+proposition
   fixes S :: "'a::euclidean_space set"
   assumes "compact S" and 0: "0 \<in> rel_interior S"
       and star: "\<And>x. x \<in> S \<Longrightarrow> open_segment 0 x \<subseteq> rel_interior S"
     shows starlike_compact_projective1_0:
             "S - rel_interior S homeomorphic sphere 0 1 \<inter> affine hull S"

     apply (subst homeomorphic_sym)
     apply (rule homeomorphic_compact [OF co01 cont_nosp2 [unfolded o_def] im_cball inj_cball])
     done
 qed
 
-corollary (* FIXME needs name *)
+corollary
   fixes S :: "'a::euclidean_space set"
   assumes "compact S" and a: "a \<in> rel_interior S"
       and star: "\<And>x. x \<in> S \<Longrightarrow> open_segment a x \<subseteq> rel_interior S"
     shows starlike_compact_projective1:
             "S - rel_interior S homeomorphic sphere a 1 \<inter> affine hull S"