src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy

 
 header {* Convex sets, functions and related things. *}
 
 theory Convex_Euclidean_Space
 imports
-  Ordered_Euclidean_Space
+  Topology_Euclidean_Space
   "~~/src/HOL/Library/Convex"
   "~~/src/HOL/Library/Set_Algebras"
 begin
 
 

   shows "rel_interior {a .. b} = {a <..< b}"
 proof -
   have "box a b \<noteq> {}"
     using assms
     unfolding set_eq_iff
-    by (auto intro!: exI[of _ "(a + b) / 2"] simp: box)
+    by (auto intro!: exI[of _ "(a + b) / 2"] simp: box_def)
   then show ?thesis
     using interior_rel_interior_gen[of "cbox a b", symmetric]
     by (simp split: split_if_asm del: box_real add: box_real[symmetric] interior_cbox)
 qed
 

   shows "is_interval s \<Longrightarrow> connected s"
   using is_interval_convex convex_connected by auto
 
 lemma convex_box: "convex (cbox a b)" "convex (box a (b::'a::euclidean_space))"
   apply (rule_tac[!] is_interval_convex)+
-  using is_interval_interval
+  using is_interval_box is_interval_cbox
   apply auto
   done
 
 subsection {* On @{text "real"}, @{text "is_interval"}, @{text "convex"} and @{text "connected"} are all equivalent. *}