src/HOL/Multivariate_Analysis/Integration.thy

   assumes incl: "{c..d} \<subseteq> {a..b::'a::ordered_euclidean_space}"
     and nonempty: "{c..d} \<noteq> {}"
   obtains p where "p division_of {a..b}" "{c..d} \<in> p"
 proof
   let ?B = "\<lambda>f::'a\<Rightarrow>'a \<times> 'a. {(\<Sum>i\<in>Basis. (fst (f i) \<bullet> i) *\<^sub>R i) .. (\<Sum>i\<in>Basis. (snd (f i) \<bullet> i) *\<^sub>R i)}"
-  def p \<equiv> "?B ` (Basis \<rightarrow>\<^isub>E {(a, c), (c, d), (d, b)})"
+  def p \<equiv> "?B ` (Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)})"
 
   show "{c .. d} \<in> p"
     unfolding p_def
     by (auto simp add: interval_eq_empty eucl_le[where 'a='a]
              intro!: image_eqI[where x="\<lambda>(i::'a)\<in>Basis. (c, d)"])

   proof (rule division_ofI)
     show "finite p" unfolding p_def by (auto intro!: finite_PiE)
     {
       fix k
       assume "k \<in> p"
-      then obtain f where f: "f \<in> Basis \<rightarrow>\<^isub>E {(a, c), (c, d), (d, b)}" and k: "k = ?B f"
+      then obtain f where f: "f \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}" and k: "k = ?B f"
         by (auto simp: p_def)
       then show "\<exists>a b. k = {a..b}" by auto
       have "k \<subseteq> {a..b} \<and> k \<noteq> {}"
       proof (simp add: k interval_eq_empty subset_interval not_less, safe)
         fix i :: 'a assume i: "i \<in> Basis"

           by (auto simp: subset_iff eucl_le[where 'a='a])
       qed
       then show "k \<noteq> {}" "k \<subseteq> {a .. b}" by auto
       {
         fix l assume "l \<in> p"
-        then obtain g where g: "g \<in> Basis \<rightarrow>\<^isub>E {(a, c), (c, d), (d, b)}" and l: "l = ?B g"
+        then obtain g where g: "g \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}" and l: "l = ?B g"
           by (auto simp: p_def)
         assume "l \<noteq> k"
         have "\<exists>i\<in>Basis. f i \<noteq> g i"
         proof (rule ccontr)
           assume "\<not> (\<exists>i\<in>Basis. f i \<noteq> g i)"

           by (auto simp: eucl_le[where 'a='a])
         then show "\<exists>l. x \<bullet> i \<in> {fst l \<bullet> i .. snd l \<bullet> i} \<and> l \<in> {(a, c), (c, d), (d, b)}"
           by auto
       qed
       then guess f unfolding bchoice_iff .. note f = this
-      moreover then have "restrict f Basis \<in> Basis \<rightarrow>\<^isub>E {(a, c), (c, d), (d, b)}"
+      moreover then have "restrict f Basis \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}"
         by auto
       moreover from f have "x \<in> ?B (restrict f Basis)"
         by (auto simp: mem_interval eucl_le[where 'a='a])
       ultimately have "\<exists>k\<in>p. x \<in> k"
         unfolding p_def by blast }