src/HOL/Multivariate_Analysis/Integration.thy

     note p = this division_ofD[OF this(1)]
     have "interior (cbox a b \<inter> \<Union>(p - {cbox u v})) = interior(cbox u v \<inter> \<Union>(p - {cbox u v}))"
       apply (rule arg_cong[of _ _ interior])
       using p(8) uv by auto
     also have "\<dots> = {}"
-      unfolding interior_inter
+      unfolding interior_Int
       apply (rule inter_interior_unions_intervals)
       using p(6) p(7)[OF p(2)] p(3)
       apply auto
       done
     finally have [simp]: "interior (cbox a b) \<inter> interior (\<Union>(p - {cbox u v})) = {}" by simp

             "cbox m n \<in> snd ` p" "cbox u v \<in> snd ` p"
             "cbox m n \<noteq> cbox u v"
             "cbox m n \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} = cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}"
           have "(cbox m n \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<inter> (cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<subseteq> cbox m n \<inter> cbox u v"
             by blast
-          note interior_mono[OF this, unfolded division_ofD(5)[OF p'' as(1-3)] interior_inter[of "cbox m n"]]
+          note interior_mono[OF this, unfolded division_ofD(5)[OF p'' as(1-3)] interior_Int[of "cbox m n"]]
           then have "interior (cbox m n \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = {}"
             unfolding as Int_absorb by auto
           then show "content (cbox m n \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = 0"
             unfolding interval_doublesplit[OF k] content_eq_0_interior[symmetric] .
         qed

               assume k: "(a, k) \<in> p" "(a, k') \<in> p" "content k \<noteq> 0" "content k' \<noteq> 0"
               guess v using pa[OF k(1)] .. note v = conjunctD2[OF this]
               guess v' using pa[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = "min v v'"
               have "box a ?v \<subseteq> k \<inter> k'"
                 unfolding v v' by (auto simp add: mem_box)
-              note interior_mono[OF this,unfolded interior_inter]
+              note interior_mono[OF this,unfolded interior_Int]
               moreover have "(a + ?v)/2 \<in> box a ?v"
                 using k(3-)
                 unfolding v v' content_eq_0 not_le
                 by (auto simp add: mem_box)
               ultimately have "(a + ?v)/2 \<in> interior k \<inter> interior k'"

               guess v using pb[OF k(1)] .. note v = conjunctD2[OF this]
               guess v' using pb[OF k(2)] .. note v' = conjunctD2[OF this]
               let ?v = "max v v'"
               have "box ?v b \<subseteq> k \<inter> k'"
                 unfolding v v' by (auto simp: mem_box)
-                note interior_mono[OF this,unfolded interior_inter]
+                note interior_mono[OF this,unfolded interior_Int]
               moreover have " ((b + ?v)/2) \<in> box ?v b"
                 using k(3-) unfolding v v' content_eq_0 not_le by (auto simp: mem_box)
               ultimately have " ((b + ?v)/2) \<in> interior k \<inter> interior k'"
                 unfolding interior_open[OF open_box] by auto
               then have *: "k = k'"

 proof -
   have "{x \<in> s. f x \<in> {y}} = {} \<or> {x \<in> s. f x \<in> {y}} = s"
     apply (rule assms(1)[unfolded connected_clopen,rule_format])
     apply rule
     defer
-    apply (rule continuous_closed_in_preimage[OF assms(4) closed_singleton])
+    apply (rule continuous_closedin_preimage[OF assms(4) closed_singleton])
     apply (rule open_openin_trans[OF assms(2)])
     unfolding open_contains_ball
   proof safe
     fix x
     assume "x \<in> s"

     assume "(x, m) \<in> T1" "(x, m) \<in> T2" "T1 \<noteq> T2" "k \<in> r" "l \<in> r" "T1 = qq k" "T2 = qq l"
     note as = this(1-5)[unfolded this(6-)]
     note kl = tagged_division_ofD(3,4)[OF qq[THEN conjunct1]]
     from this(2)[OF as(4,1)] guess u v by (elim exE) note uv=this
     have *: "interior (k \<inter> l) = {}"
-      unfolding interior_inter
+      unfolding interior_Int
       apply (rule q')
       using as
       unfolding r_def
       apply auto
       done

             apply (rule finite_imageI)
             apply (rule p')
           proof goal_cases
             case prems: (1 l y)
             have "interior (k \<inter> l) \<subseteq> interior (l \<inter> y)"
-              apply (subst(2) interior_inter)
+              apply (subst(2) interior_Int)
               apply (rule Int_greatest)
               defer
               apply (subst prems(4))
               apply auto
               done

           proof goal_cases
             case prems: (1 k y)
             from d'(4)[OF this(1)] d'(4)[OF this(2)]
             guess u1 v1 u2 v2 by (elim exE) note uv=this
             have "{} = interior ((k \<inter> y) \<inter> cbox u v)"
-              apply (subst interior_inter)
+              apply (subst interior_Int)
               using d'(5)[OF prems(1-3)]
               apply auto
               done
             also have "\<dots> = interior (y \<inter> (k \<inter> cbox u v))"
               by auto