src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy

   show thesis
     by (rule that [of 1]) (auto simp: True)
 next
   case False
   have "continuous_on s (norm \<circ> f)"
-    by (rule continuous_on_intros continuous_on_norm assms(2))+
+    by (rule continuous_intros continuous_on_norm assms(2))+
   with False obtain x where x: "x \<in> s" "\<forall>y\<in>s. (norm \<circ> f) x \<le> (norm \<circ> f) y"
     using continuous_attains_inf[OF assms(1), of "norm \<circ> f"]
     unfolding o_def
     by auto
   have "(norm \<circ> f) x > 0"

   then have *: "\<not> (\<exists>x\<in>unit_cube. f x - x = 0)"
     by auto
   obtain d where
       d: "d > 0" "\<And>x. x \<in> unit_cube \<Longrightarrow> d \<le> norm (f x - x)"
     apply (rule brouwer_compactness_lemma[OF compact_unit_cube _ *])
-    apply (rule continuous_on_intros assms)+
+    apply (rule continuous_intros assms)+
     apply blast
     done
   have *: "\<forall>x. x \<in> unit_cube \<longrightarrow> f x \<in> unit_cube"
     "\<forall>x. x \<in> (unit_cube::'a set) \<longrightarrow> (\<forall>i\<in>Basis. True \<longrightarrow> 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1)"
     using assms(2)[unfolded image_subset_iff Ball_def]

     apply (erule conjE)
     apply (rule brouwer_ball[OF assms])
     apply assumption+
     apply (rule_tac x=x in bexI)
     apply assumption+
-    apply (rule continuous_on_intros)+
+    apply (rule continuous_intros)+
     unfolding frontier_cball subset_eq Ball_def image_iff
     apply rule
     apply rule
     apply (erule bexE)
     unfolding dist_norm