diff -r 7c717ba55a0b -r fb9ae0727548 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Apr 02 18:35:02 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Apr 02 18:35:07 2014 +0200
@@ -678,7 +678,7 @@
     show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative
         (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
       by (intro has_derivative_intros assms(3)[rule_format,OF x] mult_right_has_derivative)
-  qed (insert assms(1,2), auto intro!: continuous_on_intros simp: field_simps)
+  qed (insert assms(1,2), auto intro!: continuous_intros simp: field_simps)
   then obtain x where
     "x \<in> {a <..< b}"
     "(\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)" ..
@@ -749,7 +749,7 @@
   have "\<exists>x\<in>{a<..<b}. (f b - f a) \<bullet> f b - (f b - f a) \<bullet> f a = (f b - f a) \<bullet> f' x (b - a)"
     apply (rule mvt)
     apply (rule assms(1))
-    apply (intro continuous_on_intros assms(2))
+    apply (intro continuous_intros assms(2))
     using assms(3)
     apply (fast intro: has_derivative_inner_right)
     done
@@ -798,7 +798,7 @@
     by (auto simp add: algebra_simps)
   then have 1: "continuous_on {0 .. 1} (f \<circ> ?p)"
     apply -
-    apply (rule continuous_on_intros)+
+    apply (rule continuous_intros)+
     unfolding continuous_on_eq_continuous_within
     apply rule
     apply (rule differentiable_imp_continuous_within)
@@ -1138,7 +1138,7 @@
   show ?thesis
     unfolding *
     apply (rule brouwer[OF assms(1-3), of "\<lambda>y. x + (y - f y)"])
-    apply (rule continuous_on_intros assms)+
+    apply (rule continuous_intros assms)+
     using assms(4-6)
     apply auto
     done
@@ -1209,7 +1209,7 @@
     show "continuous_on (cball (f x) e) (\<lambda>y. f (x + g' (y - f x)))"
       unfolding g'.diff
       apply (rule continuous_on_compose[of _ _ f, unfolded o_def])
-      apply (rule continuous_on_intros linear_continuous_on[OF assms(5)])+
+      apply (rule continuous_intros linear_continuous_on[OF assms(5)])+
       apply (rule continuous_on_subset[OF assms(2)])
       apply rule
       apply (unfold image_iff)