# HG changeset patch
# User immler
# Date 1387210102 -3600
# Node ID 2d3df8633dad6fb6cf065c153b25fe9f8496144c
# Parent  81290fe85890e562e6488ccf1bc1909d54d159fc
prefer box over greaterThanLessThan on euclidean_space

diff -r 81290fe85890 -r 2d3df8633dad src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Mon Dec 16 14:49:18 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Mon Dec 16 17:08:22 2013 +0100
@@ -4241,7 +4241,7 @@
   have "{a..b} \<noteq> {}"
     using assms by auto
   with i have *: "a\<bullet>i \<le> b\<bullet>i" "u\<bullet>i \<le> v\<bullet>i"
-    using assms(2) by (auto simp add: interval_eq_empty not_less)
+    using assms(2) by (auto simp add: interval_eq_empty interval)
   have x: "a\<bullet>i\<le>x\<bullet>i" "x\<bullet>i\<le>b\<bullet>i"
     using assms(1)[unfolded mem_interval] using i by auto
   have "0 \<le> (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
diff -r 81290fe85890 -r 2d3df8633dad src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon Dec 16 14:49:18 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon Dec 16 17:08:22 2013 +0100
@@ -903,23 +903,23 @@
 qed
 
 lemma interval_cart:
-  fixes a :: "'a::ord^'n"
-  shows "{a <..< b} = {x::'a^'n. \<forall>i. a$i < x$i \<and> x$i < b$i}"
-    and "{a .. b} = {x::'a^'n. \<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i}"
-  by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def)
+  fixes a :: "real^'n"
+  shows "box a b = {x::real^'n. \<forall>i. a$i < x$i \<and> x$i < b$i}"
+    and "{a .. b} = {x::real^'n. \<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i}"
+  by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def mem_interval Basis_vec_def inner_axis)
 
 lemma mem_interval_cart:
-  fixes a :: "'a::ord^'n"
-  shows "x \<in> {a<..<b} \<longleftrightarrow> (\<forall>i. a$i < x$i \<and> x$i < b$i)"
+  fixes a :: "real^'n"
+  shows "x \<in> box a b \<longleftrightarrow> (\<forall>i. a$i < x$i \<and> x$i < b$i)"
     and "x \<in> {a .. b} \<longleftrightarrow> (\<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i)"
   using interval_cart[of a b] by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def)
 
 lemma interval_eq_empty_cart:
   fixes a :: "real^'n"
-  shows "({a <..< b} = {} \<longleftrightarrow> (\<exists>i. b$i \<le> a$i))" (is ?th1)
+  shows "(box a b = {} \<longleftrightarrow> (\<exists>i. b$i \<le> a$i))" (is ?th1)
     and "({a  ..  b} = {} \<longleftrightarrow> (\<exists>i. b$i < a$i))" (is ?th2)
 proof -
-  { fix i x assume as:"b$i \<le> a$i" and x:"x\<in>{a <..< b}"
+  { fix i x assume as:"b$i \<le> a$i" and x:"x\<in>box a b"
     hence "a $ i < x $ i \<and> x $ i < b $ i" unfolding mem_interval_cart by auto
     hence "a$i < b$i" by auto
     hence False using as by auto }
@@ -931,7 +931,7 @@
       hence "a$i < ((1/2) *\<^sub>R (a+b)) $ i" "((1/2) *\<^sub>R (a+b)) $ i < b$i"
         unfolding vector_smult_component and vector_add_component
         by auto }
-    hence "{a <..< b} \<noteq> {}" using mem_interval_cart(1)[of "?x" a b] by auto }
+    hence "box a b \<noteq> {}" using mem_interval_cart(1)[of "?x" a b] by auto }
   ultimately show ?th1 by blast
 
   { fix i x assume as:"b$i < a$i" and x:"x\<in>{a .. b}"
@@ -953,16 +953,16 @@
 lemma interval_ne_empty_cart:
   fixes a :: "real^'n"
   shows "{a  ..  b} \<noteq> {} \<longleftrightarrow> (\<forall>i. a$i \<le> b$i)"
-    and "{a <..< b} \<noteq> {} \<longleftrightarrow> (\<forall>i. a$i < b$i)"
+    and "box a b \<noteq> {} \<longleftrightarrow> (\<forall>i. a$i < b$i)"
   unfolding interval_eq_empty_cart[of a b] by (auto simp add: not_less not_le)
     (* BH: Why doesn't just "auto" work here? *)
 
 lemma subset_interval_imp_cart:
   fixes a :: "real^'n"
   shows "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> {c .. d} \<subseteq> {a .. b}"
-    and "(\<forall>i. a$i < c$i \<and> d$i < b$i) \<Longrightarrow> {c .. d} \<subseteq> {a<..<b}"
-    and "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> {c<..<d} \<subseteq> {a .. b}"
-    and "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> {c<..<d} \<subseteq> {a<..<b}"
+    and "(\<forall>i. a$i < c$i \<and> d$i < b$i) \<Longrightarrow> {c .. d} \<subseteq> box a b"
+    and "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> box c d \<subseteq> {a .. b}"
+    and "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> box c d \<subseteq> box a b"
   unfolding subset_eq[unfolded Ball_def] unfolding mem_interval_cart
   by (auto intro: order_trans less_le_trans le_less_trans less_imp_le) (* BH: Why doesn't just "auto" work here? *)
 
@@ -975,21 +975,21 @@
   done
 
 lemma interval_open_subset_closed_cart:
-  fixes a :: "'a::preorder^'n"
-  shows "{a<..<b} \<subseteq> {a .. b}"
+  fixes a :: "real^'n"
+  shows "box a b \<subseteq> {a .. b}"
 proof (simp add: subset_eq, rule)
   fix x
-  assume x: "x \<in>{a<..<b}"
+  assume x: "x \<in>box a b"
   { fix i
     have "a $ i \<le> x $ i"
       using x order_less_imp_le[of "a$i" "x$i"]
-      by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff)
+      by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff mem_interval Basis_vec_def inner_axis)
   }
   moreover
   { fix i
     have "x $ i \<le> b $ i"
       using x order_less_imp_le[of "x$i" "b$i"]
-      by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff)
+      by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff mem_interval Basis_vec_def inner_axis)
   }
   ultimately
   show "a \<le> x \<and> x \<le> b"
@@ -999,21 +999,21 @@
 lemma subset_interval_cart:
   fixes a :: "real^'n"
   shows "{c .. d} \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i. c$i \<le> d$i) --> (\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i)" (is ?th1)
-    and "{c .. d} \<subseteq> {a<..<b} \<longleftrightarrow> (\<forall>i. c$i \<le> d$i) --> (\<forall>i. a$i < c$i \<and> d$i < b$i)" (is ?th2)
-    and "{c<..<d} \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i. c$i < d$i) --> (\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i)" (is ?th3)
-    and "{c<..<d} \<subseteq> {a<..<b} \<longleftrightarrow> (\<forall>i. c$i < d$i) --> (\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i)" (is ?th4)
+    and "{c .. d} \<subseteq> box a b \<longleftrightarrow> (\<forall>i. c$i \<le> d$i) --> (\<forall>i. a$i < c$i \<and> d$i < b$i)" (is ?th2)
+    and "box c d \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i. c$i < d$i) --> (\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i)" (is ?th3)
+    and "box c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i. c$i < d$i) --> (\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i)" (is ?th4)
   using subset_interval[of c d a b] by (simp_all add: Basis_vec_def inner_axis)
 
 lemma disjoint_interval_cart:
   fixes a::"real^'n"
   shows "{a .. b} \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i. (b$i < a$i \<or> d$i < c$i \<or> b$i < c$i \<or> d$i < a$i))" (is ?th1)
-    and "{a .. b} \<inter> {c<..<d} = {} \<longleftrightarrow> (\<exists>i. (b$i < a$i \<or> d$i \<le> c$i \<or> b$i \<le> c$i \<or> d$i \<le> a$i))" (is ?th2)
-    and "{a<..<b} \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i. (b$i \<le> a$i \<or> d$i < c$i \<or> b$i \<le> c$i \<or> d$i \<le> a$i))" (is ?th3)
-    and "{a<..<b} \<inter> {c<..<d} = {} \<longleftrightarrow> (\<exists>i. (b$i \<le> a$i \<or> d$i \<le> c$i \<or> b$i \<le> c$i \<or> d$i \<le> a$i))" (is ?th4)
+    and "{a .. b} \<inter> box c d = {} \<longleftrightarrow> (\<exists>i. (b$i < a$i \<or> d$i \<le> c$i \<or> b$i \<le> c$i \<or> d$i \<le> a$i))" (is ?th2)
+    and "box a b \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i. (b$i \<le> a$i \<or> d$i < c$i \<or> b$i \<le> c$i \<or> d$i \<le> a$i))" (is ?th3)
+    and "box a b \<inter> box c d = {} \<longleftrightarrow> (\<exists>i. (b$i \<le> a$i \<or> d$i \<le> c$i \<or> b$i \<le> c$i \<or> d$i \<le> a$i))" (is ?th4)
   using disjoint_interval[of a b c d] by (simp_all add: Basis_vec_def inner_axis)
 
 lemma inter_interval_cart:
-  fixes a :: "'a::linorder^'n"
+  fixes a :: "real^'n"
   shows "{a .. b} \<inter> {c .. d} =  {(\<chi> i. max (a$i) (c$i)) .. (\<chi> i. min (b$i) (d$i))}"
   unfolding set_eq_iff and Int_iff and mem_interval_cart
   by auto
diff -r 81290fe85890 -r 2d3df8633dad src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Dec 16 14:49:18 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Dec 16 17:08:22 2013 +0100
@@ -3366,18 +3366,21 @@
   ultimately show ?thesis by auto
 qed
 
+lemma box_real: "box a b = {a<..<b::real}"
+  by (force simp add: box_def)
+
 lemma rel_interior_real_interval:
   fixes a b :: real
   assumes "a < b"
   shows "rel_interior {a..b} = {a<..<b}"
 proof -
-  have "{a<..<b} \<noteq> {}"
+  have "box a b \<noteq> {}"
     using assms
     unfolding set_eq_iff
-    by (auto intro!: exI[of _ "(a + b) / 2"])
+    by (auto intro!: exI[of _ "(a + b) / 2"] simp: box_def)
   then show ?thesis
     using interior_rel_interior_gen[of "{a..b}", symmetric]
-    by (simp split: split_if_asm add: interior_closed_interval)
+    by (simp split: split_if_asm add: interior_closed_interval box_real)
 qed
 
 lemma rel_interior_real_semiline:
@@ -5666,7 +5669,7 @@
   shows "is_interval s \<Longrightarrow> connected s"
   using is_interval_convex convex_connected by auto
 
-lemma convex_interval: "convex {a .. b}" "convex {a<..<b::'a::ordered_euclidean_space}"
+lemma convex_interval: "convex {a .. b}" "convex (box a (b::'a::ordered_euclidean_space))"
   apply (rule_tac[!] is_interval_convex)
   using is_interval_interval
   apply auto
diff -r 81290fe85890 -r 2d3df8633dad src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Dec 16 14:49:18 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Dec 16 17:08:22 2013 +0100
@@ -586,12 +586,12 @@
 
 lemma frechet_derivative_unique_within_open_interval:
   fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
-  assumes "x \<in> {a<..<b}"
-    and "(f has_derivative f' ) (at x within {a<..<b})"
-    and "(f has_derivative f'') (at x within {a<..<b})"
+  assumes "x \<in> box a b"
+    and "(f has_derivative f' ) (at x within box a b)"
+    and "(f has_derivative f'') (at x within box a b)"
   shows "f' = f''"
 proof -
-  from assms(1) have *: "at x within {a<..<b} = at x"
+  from assms(1) have *: "at x within box a b = at x"
     by (metis at_within_interior interior_open open_interval)
   from assms(2,3) [unfolded *] show "f' = f''"
     by (rule frechet_derivative_unique_at)
@@ -741,10 +741,10 @@
   assumes "a < b"
     and "f a = f b"
     and "continuous_on {a..b} f"
-    and "\<forall>x\<in>{a<..<b}. (f has_derivative f' x) (at x)"
-  shows "\<exists>x\<in>{a<..<b}. f' x = (\<lambda>v. 0)"
+    and "\<forall>x\<in>box a b. (f has_derivative f' x) (at x)"
+  shows "\<exists>x\<in>box a b. f' x = (\<lambda>v. 0)"
 proof -
-  have "\<exists>x\<in>{a<..<b}. (\<forall>y\<in>{a<..<b}. f x \<le> f y) \<or> (\<forall>y\<in>{a<..<b}. f y \<le> f x)"
+  have "\<exists>x\<in>box a b. (\<forall>y\<in>box a b. f x \<le> f y) \<or> (\<forall>y\<in>box a b. f y \<le> f x)"
   proof -
     have "(a + b) / 2 \<in> {a .. b}"
       using assms(1) by auto
@@ -753,20 +753,20 @@
     guess d using continuous_attains_sup[OF compact_interval * assms(3)] .. note d=this
     guess c using continuous_attains_inf[OF compact_interval * assms(3)] .. note c=this
     show ?thesis
-    proof (cases "d \<in> {a<..<b} \<or> c \<in> {a<..<b}")
+    proof (cases "d \<in> box a b \<or> c \<in> box a b")
       case True
       then show ?thesis
         apply (erule_tac disjE)
         apply (rule_tac x=d in bexI)
         apply (rule_tac[3] x=c in bexI)
         using d c
-        apply auto
+        apply (auto simp: box_real)
         done
     next
       def e \<equiv> "(a + b) /2"
       case False
       then have "f d = f c"
-        using d c assms(2) by auto
+        using d c assms(2) by (auto simp: box_real)
       then have "\<And>x. x \<in> {a..b} \<Longrightarrow> f x = f d"
         using c d
         apply -
@@ -777,13 +777,13 @@
         apply (rule_tac x=e in bexI)
         unfolding e_def
         using assms(1)
-        apply auto
+        apply (auto simp: box_real)
         done
     qed
   qed
   then guess x .. note x=this
   then have "f' x = (\<lambda>v. 0)"
-    apply (rule_tac differential_zero_maxmin[of x "{a<..<b}" f "f' x"])
+    apply (rule_tac differential_zero_maxmin[of x "box a b" f "f' x"])
     defer
     apply (rule open_interval)
     apply (rule assms(4)[unfolded has_derivative_at[symmetric],THEN bspec[where x=x]])
@@ -813,10 +813,10 @@
   assumes "\<forall>x\<in>{a<..<b}. (f has_derivative (f' x)) (at x)"
   shows "\<exists>x\<in>{a<..<b}. f b - f a = (f' x) (b - a)"
 proof -
-  have "\<exists>x\<in>{a<..<b}. (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)"
+  have "\<exists>x\<in>box a b. (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)"
   proof (intro rolle[OF assms(1), of "\<lambda>x. f x - (f b - f a) / (b - a) * x"] ballI)
     fix x
-    assume x: "x \<in> {a<..<b}"
+    assume "x \<in> box a b" hence x: "x \<in> {a<..<b}" by (simp add: box_real)
     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 FDERIV_intros assms(3)[rule_format,OF x] mult_right_has_derivative)
@@ -825,7 +825,7 @@
   then show ?thesis
     apply (rule_tac x=x in bexI)
     apply (drule fun_cong[of _ _ "b - a"])
-    apply auto
+    apply (auto simp: box_real)
     done
 qed
 
@@ -841,13 +841,13 @@
   defer
 proof
   fix x
-  assume x: "x \<in> {a<..<b}"
+  assume x: "x \<in> {a<..<b}" hence x: "x \<in> box a b" by (simp add: box_real)
   show "(f has_derivative f' x) (at x)"
     unfolding has_derivative_within_open[OF x open_interval,symmetric]
     apply (rule has_derivative_within_subset)
     apply (rule assms(2)[rule_format])
     using x
-    apply auto
+    apply (auto simp: box_real)
     done
 qed (insert assms(2), auto)
 
@@ -963,8 +963,7 @@
       apply auto
       done
     then show ?case
-      unfolding has_derivative_within_open[OF goal1 open_interval]
-      by auto
+      unfolding has_derivative_within_open[OF goal1 open_greaterThanLessThan] .
   qed
   guess u using mvt_general[OF zero_less_one 1 2] .. note u = this
   have **: "\<And>x y. x \<in> s \<Longrightarrow> norm (f' x y) \<le> B * norm y"
diff -r 81290fe85890 -r 2d3df8633dad src/HOL/Multivariate_Analysis/Fashoda.thy
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Mon Dec 16 14:49:18 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Mon Dec 16 17:08:22 2013 +0100
@@ -80,7 +80,7 @@
   } note x0 = this
   have 21: "\<And>i::2. i \<noteq> 1 \<Longrightarrow> i = 2"
     using UNIV_2 by auto
-  have 1: "{- 1<..<1::real^2} \<noteq> {}"
+  have 1: "box (- 1) (1::real^2) \<noteq> {}"
     unfolding interval_eq_empty_cart by auto
   have 2: "continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)"
     apply (intro continuous_on_intros continuous_on_component)
@@ -344,7 +344,7 @@
     by auto
 next
   have "{a..b} \<noteq> {}"
-    using assms(3) using path_image_nonempty by auto
+    using assms(3) using path_image_nonempty[of f] by auto
   then have "a \<le> b"
     unfolding interval_eq_empty_cart less_eq_vec_def by (auto simp add: not_less)
   then show "a$1 = b$1 \<or> a$2 = b$2 \<or> (a$1 < b$1 \<and> a$2 < b$2)"
@@ -646,7 +646,7 @@
   obtains z where "z \<in> path_image f" and "z \<in> path_image g"
 proof -
   have "{a..b} \<noteq> {}"
-    using path_image_nonempty using assms(3) by auto
+    using path_image_nonempty[of f] using assms(3) by auto
   note ab=this[unfolded interval_eq_empty_cart not_ex forall_2 not_less]
   have "pathstart f \<in> {a..b}"
     and "pathfinish f \<in> {a..b}"
@@ -692,7 +692,7 @@
       using ab startfin abab assms(3)
       using assms(9-)
       unfolding assms
-      apply (auto simp add: field_simps)
+      apply (auto simp add: field_simps interval)
       done
     then show "path_image ?P1 \<subseteq> {?a .. ?b}" .
     have "path_image ?P2 \<subseteq> {?a .. ?b}"
@@ -704,7 +704,7 @@
       using ab startfin abab assms(4)
       using assms(9-)
       unfolding assms
-      apply (auto simp add: field_simps)
+      apply (auto simp add: field_simps interval)
       done
     then show "path_image ?P2 \<subseteq> {?a .. ?b}" .
     show "a $ 1 - 2 = a $ 1 - 2"
diff -r 81290fe85890 -r 2d3df8633dad src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Dec 16 14:49:18 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Dec 16 17:08:22 2013 +0100
@@ -220,7 +220,8 @@
   where "One \<equiv> \<Sum>Basis"
 
 lemma empty_as_interval: "{} = {One..(0::'a::ordered_euclidean_space)}"
-  by (auto simp: set_eq_iff eucl_le[where 'a='a] intro!: bexI[OF _ SOME_Basis])
+  apply (auto simp: eucl_le[where 'a='a])
+  by (metis (mono_tags) eucl_less eucl_less_not_refl order.strict_trans2 zero_less_one)
 
 lemma interior_subset_union_intervals:
   assumes "i = {a..b::'a::ordered_euclidean_space}"
@@ -230,11 +231,11 @@
     and "interior i \<inter> interior j = {}"
   shows "interior i \<subseteq> interior s"
 proof -
-  have "{a<..<b} \<inter> {c..d} = {}"
+  have "box a b \<inter> {c..d} = {}"
     using inter_interval_mixed_eq_empty[of c d a b] and assms(3,5)
     unfolding assms(1,2) interior_closed_interval by auto
   moreover
-  have "{a<..<b} \<subseteq> {c..d} \<union> s"
+  have "box a b \<subseteq> {c..d} \<union> s"
     apply (rule order_trans,rule interval_open_subset_closed)
     using assms(4) unfolding assms(1,2)
     apply auto
@@ -310,9 +311,9 @@
         then show ?thesis by auto
       next
         case True show ?thesis
-        proof (cases "x\<in>{a<..<b}")
+        proof (cases "x\<in>box a b")
           case True
-          then obtain d where "0 < d \<and> ball x d \<subseteq> {a<..<b}"
+          then obtain d where "0 < d \<and> ball x d \<subseteq> box a b"
             unfolding open_contains_ball_eq[OF open_interval,rule_format] ..
           then show ?thesis
             apply (rule_tac x=i in bexI, rule_tac x=x in exI, rule_tac x="min d e" in exI)
@@ -1114,7 +1115,8 @@
     obtain c d where k: "k = {c..d}"
       using p(4)[OF goal1] by blast
     have *: "{c..d} \<subseteq> {a..b}" "{c..d} \<noteq> {}"
-      using p(2,3)[OF goal1, unfolded k] using assms(2) by auto
+      using p(2,3)[OF goal1, unfolded k] using assms(2)
+        by auto
     obtain q where "q division_of {a..b}" "{c..d} \<in> q"
       by (rule partial_division_extend_1[OF *])
     then show ?case
@@ -1324,7 +1326,7 @@
       apply (rule assm(1)) unfolding Union_insert
       using assm(2-4) as
       apply -
-      apply (fastforce dest: assm(5))+
+      apply (fast dest: assm(5))+
       done
   next
     assume as: "p \<noteq> {}" "interior {a..b} \<noteq> {}" "{a..b} \<noteq> {}"
@@ -2149,7 +2151,7 @@
       unfolding s t interior_closed_interval
     proof (rule *)
       fix x
-      assume "x \<in> {c<..<d}" "x \<in> {e<..<f}"
+      assume "x \<in> box c d" "x \<in> box e f"
       then have x: "c\<bullet>i < d\<bullet>i" "e\<bullet>i < f\<bullet>i" "c\<bullet>i < f\<bullet>i" "e\<bullet>i < d\<bullet>i"
         unfolding mem_interval using i'
         apply -
@@ -3274,7 +3276,7 @@
   then have "{a .. b} = {}"
     unfolding interval_eq_empty by (auto simp: eucl_le[where 'a='a] not_le)
   then show ?thesis
-    by auto
+    by (auto simp: not_le)
 qed
 
 lemma division_split_left_inj:
@@ -3405,7 +3407,7 @@
       apply -
       prefer 3
       apply (subst interval_split[OF k])
-      apply auto
+      apply (auto intro: order.trans)
       done
     fix k'
     assume "k' \<in> ?p1"
@@ -3426,7 +3428,7 @@
       apply -
       prefer 3
       apply (subst interval_split[OF k])
-      apply auto
+      apply (auto intro: order.trans)
       done
     fix k'
     assume "k' \<in> ?p2"
@@ -3721,7 +3723,7 @@
     apply (rule tagged_division_union[OF assms(1-2)])
     unfolding interval_split[OF k] interior_closed_interval
     using k
-    apply (auto simp add: eucl_less[where 'a='a] elim!: ballE[where x=k])
+    apply (auto simp add: eucl_less[where 'a='a] interval elim!: ballE[where x=k])
     done
 qed
 
@@ -6248,10 +6250,10 @@
 
 subsection {* In particular, the boundary of an interval is negligible. *}
 
-lemma negligible_frontier_interval: "negligible({a::'a::ordered_euclidean_space..b} - {a<..<b})"
+lemma negligible_frontier_interval: "negligible({a::'a::ordered_euclidean_space..b} - box a b)"
 proof -
   let ?A = "\<Union>((\<lambda>k. {x. x\<bullet>k = a\<bullet>k} \<union> {x::'a. x\<bullet>k = b\<bullet>k}) ` Basis)"
-  have "{a..b} - {a<..<b} \<subseteq> ?A"
+  have "{a..b} - box a b \<subseteq> ?A"
     apply rule unfolding Diff_iff mem_interval
     apply simp
     apply(erule conjE bexE)+
@@ -6267,7 +6269,7 @@
 qed
 
 lemma has_integral_spike_interior:
-  assumes "\<forall>x\<in>{a<..<b}. g x = f x"
+  assumes "\<forall>x\<in>box a b. g x = f x"
     and "(f has_integral y) ({a..b})"
   shows "(g has_integral y) {a..b}"
   apply (rule has_integral_spike[OF negligible_frontier_interval _ assms(2)])
@@ -6276,7 +6278,7 @@
   done
 
 lemma has_integral_spike_interior_eq:
-  assumes "\<forall>x\<in>{a<..<b}. g x = f x"
+  assumes "\<forall>x\<in>box a b. g x = f x"
   shows "(f has_integral y) {a..b} \<longleftrightarrow> (g has_integral y) {a..b}"
   apply rule
   apply (rule_tac[!] has_integral_spike_interior)
@@ -6285,7 +6287,7 @@
   done
 
 lemma integrable_spike_interior:
-  assumes "\<forall>x\<in>{a<..<b}. g x = f x"
+  assumes "\<forall>x\<in>box a b. g x = f x"
     and "f integrable_on {a..b}"
   shows "g integrable_on {a..b}"
   using assms
@@ -7029,7 +7031,7 @@
     then show "f integrable_on k"
       apply safe
       apply (rule d[THEN conjunct2,rule_format,of x])
-      apply auto
+      apply (auto intro: order.trans)
       done
   qed
 qed
@@ -7650,7 +7652,7 @@
   fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
   assumes "a \<le> b"
     and "continuous_on {a..b} f"
-    and "\<forall>x\<in>{a<..<b}. (f has_vector_derivative f'(x)) (at x)"
+    and "\<forall>x\<in>box a b. (f has_vector_derivative f'(x)) (at x)"
   shows "(f' has_integral (f b - f a)) {a..b}"
 proof -
   {
@@ -7682,7 +7684,7 @@
   note assms(3)[unfolded has_vector_derivative_def has_derivative_at_alt ball_conj_distrib]
   note conjunctD2[OF this]
   note bounded=this(1) and this(2)
-  from this(2) have "\<forall>x\<in>{a<..<b}. \<exists>d>0. \<forall>y. norm (y - x) < d \<longrightarrow>
+  from this(2) have "\<forall>x\<in>box a b. \<exists>d>0. \<forall>y. norm (y - x) < d \<longrightarrow>
     norm (f y - f x - (y - x) *\<^sub>R f' x) \<le> e/2 * norm (y - x)"
     apply -
     apply safe
@@ -7885,8 +7887,8 @@
         note result = as(2)[unfolded k interval_bounds_real[OF this(1)] content_real[OF this(1)]]
 
         assume as': "x \<noteq> a" "x \<noteq> b"
-        then have "x \<in> {a<..<b}"
-          using p(2-3)[OF as(1)] by auto
+        then have "x \<in> box a b"
+          using p(2-3)[OF as(1)] by (auto simp: interval)
         note  * = d(2)[OF this]
         have "norm ((v - u) *\<^sub>R f' (x) - (f (v) - f (u))) =
           norm ((f (u) - f (x) - (u - x) *\<^sub>R f' (x)) - (f (v) - f (x) - (v - x) *\<^sub>R f' (x)))"
@@ -8047,13 +8049,13 @@
               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 "{a <..< ?v} \<subseteq> k \<inter> k'"
-                unfolding v v' by (auto simp add:)
+              have "box a ?v \<subseteq> k \<inter> k'"
+                unfolding v v' by (auto simp add: interval)
               note interior_mono[OF this,unfolded interior_inter]
-              moreover have "(a + ?v)/2 \<in> { a <..< ?v}"
+              moreover have "(a + ?v)/2 \<in> box a ?v"
                 using k(3-)
                 unfolding v v' content_eq_0 not_le
-                by (auto simp add: not_le)
+                by (auto simp add: interval)
               ultimately have "(a + ?v)/2 \<in> interior k \<inter> interior k'"
                 unfolding interior_open[OF open_interval] by auto
               then have *: "k = k'"
@@ -8078,11 +8080,11 @@
               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 "{?v <..< b} \<subseteq> k \<inter> k'"
-                unfolding v v' by auto
+              have "box ?v b \<subseteq> k \<inter> k'"
+                unfolding v v' by (auto simp: interval)
                 note interior_mono[OF this,unfolded interior_inter]
-              moreover have " ((b + ?v)/2) \<in> {?v <..<  b}"
-                using k(3-) unfolding v v' content_eq_0 not_le by auto
+              moreover have " ((b + ?v)/2) \<in> box ?v b"
+                using k(3-) unfolding v v' content_eq_0 not_le by (auto simp: interval)
               ultimately have " ((b + ?v)/2) \<in> interior k \<inter> interior k'"
                 unfolding interior_open[OF open_interval] by auto
               then have *: "k = k'"
@@ -8175,7 +8177,7 @@
   assumes "finite s"
     and "a \<le> b"
     and "continuous_on {a..b} f"
-    and "\<forall>x\<in>{a<..<b} - s. (f has_vector_derivative f'(x)) (at x)"
+    and "\<forall>x\<in>box a b - s. (f has_vector_derivative f'(x)) (at x)"
   shows "(f' has_integral (f b - f a)) {a..b}"
   using assms
 proof (induct "card s" arbitrary: s a b)
@@ -8196,7 +8198,7 @@
     done
   note cs = this[rule_format]
   show ?case
-  proof (cases "c \<in> {a<..<b}")
+  proof (cases "c \<in> box a b")
     case False
     then show ?thesis
       apply -
@@ -8213,7 +8215,7 @@
       by auto
     case True
     then have "a \<le> c" "c \<le> b"
-      by auto
+      by (auto simp: interval)
     then show ?thesis
       apply (subst *)
       apply (rule has_integral_combine)
@@ -8225,15 +8227,15 @@
       show "continuous_on {a..c} f" "continuous_on {c..b} f"
         apply (rule_tac[!] continuous_on_subset[OF Suc(5)])
         using True
-        apply auto
-        done
-      let ?P = "\<lambda>i j. \<forall>x\<in>{i<..<j} - s'. (f has_vector_derivative f' x) (at x)"
+        apply (auto simp: interval)
+        done
+      let ?P = "\<lambda>i j. \<forall>x\<in>box i j - s'. (f has_vector_derivative f' x) (at x)"
       show "?P a c" "?P c b"
         apply safe
         apply (rule_tac[!] Suc(6)[rule_format])
         using True
         unfolding cs
-        apply auto
+        apply (auto simp: interval)
         done
     qed auto
   qed
@@ -8248,7 +8250,7 @@
   shows "(f' has_integral (f(b) - f(a))) {a..b}"
   apply (rule fundamental_theorem_of_calculus_interior_strong[OF assms(1-3), of f'])
   using assms(4)
-  apply auto
+  apply (auto simp: interval)
   done
 
 lemma indefinite_integral_continuous_left:
@@ -8609,7 +8611,7 @@
     apply (rule open_interval)
     apply (rule has_derivative_within_subset[where s="{a..b}"])
     using assms(4) assms(5)
-    apply auto
+    apply (auto simp: interval)
     done
   note this[unfolded *]
   note has_integral_unique[OF has_integral_0 this]
@@ -8773,9 +8775,9 @@
   fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::banach"
   assumes "(f has_integral i) {c..d}"
     and "{c..d} \<subseteq> {a..b}"
-  shows "((\<lambda>x. if x \<in> {c<..<d} then f x else 0) has_integral i) {a..b}"
-proof -
-  def g \<equiv> "\<lambda>x. if x \<in>{c<..<d} then f x else 0"
+  shows "((\<lambda>x. if x \<in> box c d then f x else 0) has_integral i) {a..b}"
+proof -
+  def g \<equiv> "\<lambda>x. if x \<in>box c d then f x else 0"
   {
     presume *: "{c..d} \<noteq> {} \<Longrightarrow> ?thesis"
     show ?thesis
@@ -8784,7 +8786,7 @@
       apply assumption
     proof -
       case goal1
-      then have *: "{c<..<d} = {}"
+      then have *: "box c d = {}"
         using interval_open_subset_closed
         by auto
       show ?thesis
@@ -9812,7 +9814,7 @@
     from d(5)[OF goal1] show ?case
       unfolding obt interior_closed_interval
       apply -
-      apply (rule negligible_subset[of "({a..b}-{a<..<b}) \<union> ({c..d}-{c<..<d})"])
+      apply (rule negligible_subset[of "({a..b}-box a b) \<union> ({c..d}-box c d)"])
       apply (rule negligible_union negligible_frontier_interval)+
       apply auto
       done
@@ -9944,7 +9946,7 @@
   case goal1
   note tagged_division_ofD(3-4)[OF assms(2) this]
   then show ?case
-    using integrable_subinterval[OF assms(1)] by auto
+    using integrable_subinterval[OF assms(1)] by blast
 qed
 
 lemma integral_combine_tagged_division_topdown:
diff -r 81290fe85890 -r 2d3df8633dad src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Dec 16 14:49:18 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Dec 16 17:08:22 2013 +0100
@@ -826,7 +826,14 @@
   unfolding dist_norm norm_eq_sqrt_inner setL2_def
   by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left)
 
-definition "box a b = {x. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i}"
+definition (in euclidean_space) eucl_less (infix "<e" 50)
+  where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)"
+
+definition box_eucl_less: "box a b = {x. a <e x \<and> x <e b}"
+
+lemma box_def: "box a b = {x. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i}"
+  and in_box_eucl_less: "x \<in> box a b \<longleftrightarrow> a <e x \<and> x <e b"
+  by (auto simp: box_eucl_less eucl_less_def)
 
 lemma rational_boxes:
   fixes x :: "'a\<Colon>euclidean_space"
@@ -2042,8 +2049,7 @@
       by auto
     then have "ball x (infdist x A) \<inter> closure A = {}"
       apply auto
-      apply (metis `0 < infdist x A` `x \<in> closure A` closure_approachable dist_commute
-        eucl_less_not_refl euclidean_trans(2) infdist_le)
+      apply (metis `x \<in> closure A` closure_approachable dist_commute infdist_le not_less)
       done
     then have "x \<notin> closure A"
       by (metis `0 < infdist x A` centre_in_ball disjoint_iff_not_equal)
@@ -5992,25 +5998,25 @@
 
 lemma interval:
   fixes a :: "'a::ordered_euclidean_space"
-  shows "{a <..< b} = {x::'a. \<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i}"
+  shows "box a b = {x::'a. \<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i}"
     and "{a .. b} = {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i}"
-  by (auto simp add:set_eq_iff eucl_le[where 'a='a] eucl_less[where 'a='a])
+  by (auto simp add:set_eq_iff eucl_le[where 'a='a] box_def)
 
 lemma mem_interval:
   fixes a :: "'a::ordered_euclidean_space"
-  shows "x \<in> {a<..<b} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i)"
+  shows "x \<in> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i)"
     and "x \<in> {a .. b} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i)"
   using interval[of a b]
-  by (auto simp add: set_eq_iff eucl_le[where 'a='a] eucl_less[where 'a='a])
+  by auto
 
 lemma interval_eq_empty:
   fixes a :: "'a::ordered_euclidean_space"
-  shows "({a <..< b} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i))" (is ?th1)
+  shows "(box a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i))" (is ?th1)
     and "({a  ..  b} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i < a\<bullet>i))" (is ?th2)
 proof -
   {
     fix i x
-    assume i: "i\<in>Basis" and as:"b\<bullet>i \<le> a\<bullet>i" and x:"x\<in>{a <..< b}"
+    assume i: "i\<in>Basis" and as:"b\<bullet>i \<le> a\<bullet>i" and x:"x\<in>box a b"
     then have "a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i"
       unfolding mem_interval by auto
     then have "a\<bullet>i < b\<bullet>i" by auto
@@ -6028,7 +6034,7 @@
       then have "a\<bullet>i < ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i < b\<bullet>i"
         by (auto simp: inner_add_left)
     }
-    then have "{a <..< b} \<noteq> {}"
+    then have "box a b \<noteq> {}"
       using mem_interval(1)[of "?x" a b] by auto
   }
   ultimately show ?th1 by blast
@@ -6062,37 +6068,37 @@
 lemma interval_ne_empty:
   fixes a :: "'a::ordered_euclidean_space"
   shows "{a  ..  b} \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i)"
-  and "{a <..< b} \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
+  and "box a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
   unfolding interval_eq_empty[of a b] by fastforce+
 
 lemma interval_sing:
   fixes a :: "'a::ordered_euclidean_space"
   shows "{a .. a} = {a}"
-    and "{a<..<a} = {}"
+    and "box a a = {}"
   unfolding set_eq_iff mem_interval eq_iff [symmetric]
   by (auto intro: euclidean_eqI simp: ex_in_conv)
 
 lemma subset_interval_imp:
   fixes a :: "'a::ordered_euclidean_space"
   shows "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> {c .. d} \<subseteq> {a .. b}"
-    and "(\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i) \<Longrightarrow> {c .. d} \<subseteq> {a<..<b}"
-    and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> {c<..<d} \<subseteq> {a .. b}"
-    and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> {c<..<d} \<subseteq> {a<..<b}"
+    and "(\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i) \<Longrightarrow> {c .. d} \<subseteq> box a b"
+    and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> box c d \<subseteq> {a .. b}"
+    and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> box c d \<subseteq> box a b"
   unfolding subset_eq[unfolded Ball_def] unfolding mem_interval
   by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+
 
 lemma interval_open_subset_closed:
   fixes a :: "'a::ordered_euclidean_space"
-  shows "{a<..<b} \<subseteq> {a .. b}"
+  shows "box a b \<subseteq> {a .. b}"
   unfolding subset_eq [unfolded Ball_def] mem_interval
   by (fast intro: less_imp_le)
 
 lemma subset_interval:
   fixes a :: "'a::ordered_euclidean_space"
   shows "{c .. d} \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th1)
-    and "{c .. d} \<subseteq> {a<..<b} \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i)" (is ?th2)
-    and "{c<..<d} \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th3)
-    and "{c<..<d} \<subseteq> {a<..<b} \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th4)
+    and "{c .. d} \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i)" (is ?th2)
+    and "box c d \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th3)
+    and "box c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th4)
 proof -
   show ?th1
     unfolding subset_eq and Ball_def and mem_interval
@@ -6101,8 +6107,8 @@
     unfolding subset_eq and Ball_def and mem_interval
     by (auto intro: le_less_trans less_le_trans order_trans less_imp_le)
   {
-    assume as: "{c<..<d} \<subseteq> {a .. b}" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
-    then have "{c<..<d} \<noteq> {}"
+    assume as: "box c d \<subseteq> {a .. b}" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
+    then have "box c d \<noteq> {}"
       unfolding interval_eq_empty by auto
     fix i :: 'a
     assume i: "i \<in> Basis"
@@ -6119,7 +6125,7 @@
           apply (auto simp add: as2)
           done
       }
-      then have "?x\<in>{c<..<d}"
+      then have "?x\<in>box c d"
         using i unfolding mem_interval by auto
       moreover
       have "?x \<notin> {a .. b}"
@@ -6145,7 +6151,7 @@
           apply (auto simp add: as2)
           done
       }
-      then have "?x\<in>{c<..<d}"
+      then have "?x\<in>box c d"
         unfolding mem_interval by auto
       moreover
       have "?x\<notin>{a .. b}"
@@ -6171,10 +6177,10 @@
     apply (erule_tac x=xa in allE, erule_tac x=xa in allE, fastforce)+
     done
   {
-    assume as: "{c<..<d} \<subseteq> {a<..<b}" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
+    assume as: "box c d \<subseteq> box a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
     fix i :: 'a
     assume i:"i\<in>Basis"
-    from as(1) have "{c<..<d} \<subseteq> {a..b}"
+    from as(1) have "box c d \<subseteq> {a..b}"
       using interval_open_subset_closed[of a b] by auto
     then have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
       using part1 and as(2) using i by auto
@@ -6200,9 +6206,9 @@
 lemma disjoint_interval:
   fixes a::"'a::ordered_euclidean_space"
   shows "{a .. b} \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i < a\<bullet>i \<or> d\<bullet>i < c\<bullet>i \<or> b\<bullet>i < c\<bullet>i \<or> d\<bullet>i < a\<bullet>i))" (is ?th1)
-    and "{a .. b} \<inter> {c<..<d} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i < a\<bullet>i \<or> d\<bullet>i \<le> c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th2)
-    and "{a<..<b} \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i \<le> a\<bullet>i \<or> d\<bullet>i < c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th3)
-    and "{a<..<b} \<inter> {c<..<d} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i \<le> a\<bullet>i \<or> d\<bullet>i \<le> c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th4)
+    and "{a .. b} \<inter> box c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i < a\<bullet>i \<or> d\<bullet>i \<le> c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th2)
+    and "box a b \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i \<le> a\<bullet>i \<or> d\<bullet>i < c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th3)
+    and "box a b \<inter> box c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i \<le> a\<bullet>i \<or> d\<bullet>i \<le> c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th4)
 proof -
   let ?z = "(\<Sum>i\<in>Basis. (((max (a\<bullet>i) (c\<bullet>i)) + (min (b\<bullet>i) (d\<bullet>i))) / 2) *\<^sub>R i)::'a"
   have **: "\<And>P Q. (\<And>i :: 'a. i \<in> Basis \<Longrightarrow> Q ?z i \<Longrightarrow> P i) \<Longrightarrow>
@@ -6219,14 +6225,14 @@
 
 lemma open_interval[intro]:
   fixes a b :: "'a::ordered_euclidean_space"
-  shows "open {a<..<b}"
+  shows "open (box a b)"
 proof -
   have "open (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i})"
     by (intro open_INT finite_lessThan ballI continuous_open_vimage allI
       linear_continuous_at open_real_greaterThanLessThan finite_Basis bounded_linear_inner_left)
-  also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i}) = {a<..<b}"
-    by (auto simp add: eucl_less [where 'a='a])
-  finally show "open {a<..<b}" .
+  also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i}) = box a b"
+    by (auto simp add: interval)
+  finally show "open (box a b)" .
 qed
 
 lemma closed_interval[intro]:
@@ -6243,7 +6249,7 @@
 
 lemma interior_closed_interval [intro]:
   fixes a b :: "'a::ordered_euclidean_space"
-  shows "interior {a..b} = {a<..<b}" (is "?L = ?R")
+  shows "interior {a..b} = box a b" (is "?L = ?R")
 proof(rule subset_antisym)
   show "?R \<subseteq> ?L"
     using interval_open_subset_closed open_interval
@@ -6275,7 +6281,7 @@
         using `e>0` i
         by (auto simp: inner_diff_left inner_Basis inner_add_left)
     }
-    then have "x \<in> {a<..<b}"
+    then have "x \<in> box a b"
       unfolding mem_interval by auto
   }
   then show "?L \<subseteq> ?R" ..
@@ -6309,15 +6315,15 @@
 
 lemma bounded_interval:
   fixes a :: "'a::ordered_euclidean_space"
-  shows "bounded {a .. b} \<and> bounded {a<..<b}"
+  shows "bounded {a .. b} \<and> bounded (box a b)"
   using bounded_closed_interval[of a b]
   using interval_open_subset_closed[of a b]
-  using bounded_subset[of "{a..b}" "{a<..<b}"]
+  using bounded_subset[of "{a..b}" "box a b"]
   by simp
 
 lemma not_interval_univ:
   fixes a :: "'a::ordered_euclidean_space"
-  shows "{a .. b} \<noteq> UNIV \<and> {a<..<b} \<noteq> UNIV"
+  shows "{a .. b} \<noteq> UNIV \<and> box a b \<noteq> UNIV"
   using bounded_interval[of a b] by auto
 
 lemma compact_interval:
@@ -6328,8 +6334,8 @@
 
 lemma open_interval_midpoint:
   fixes a :: "'a::ordered_euclidean_space"
-  assumes "{a<..<b} \<noteq> {}"
-  shows "((1/2) *\<^sub>R (a + b)) \<in> {a<..<b}"
+  assumes "box a b \<noteq> {}"
+  shows "((1/2) *\<^sub>R (a + b)) \<in> box a b"
 proof -
   {
     fix i :: 'a
@@ -6342,10 +6348,10 @@
 
 lemma open_closed_interval_convex:
   fixes x :: "'a::ordered_euclidean_space"
-  assumes x: "x \<in> {a<..<b}"
+  assumes x: "x \<in> box a b"
     and y: "y \<in> {a .. b}"
     and e: "0 < e" "e \<le> 1"
-  shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<in> {a<..<b}"
+  shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<in> box a b"
 proof -
   {
     fix i :: 'a
@@ -6392,14 +6398,11 @@
 
 lemma closure_open_interval:
   fixes a :: "'a::ordered_euclidean_space"
-  assumes "{a<..<b} \<noteq> {}"
-  shows "closure {a<..<b} = {a .. b}"
+  assumes "box a b \<noteq> {}"
+  shows "closure (box a b) = {a .. b}"
 proof -
-  have ab: "a < b"
-    using assms[unfolded interval_ne_empty]
-    apply (subst eucl_less)
-    apply auto
-    done
+  have ab: "a <e b"
+    using assms by (simp add: eucl_less_def interval_ne_empty)
   let ?c = "(1 / 2) *\<^sub>R (a + b)"
   {
     fix x
@@ -6407,15 +6410,15 @@
     def f \<equiv> "\<lambda>n::nat. x + (inverse (real n + 1)) *\<^sub>R (?c - x)"
     {
       fix n
-      assume fn: "f n < b \<longrightarrow> a < f n \<longrightarrow> f n = x" and xc: "x \<noteq> ?c"
+      assume fn: "f n <e b \<longrightarrow> a <e f n \<longrightarrow> f n = x" and xc: "x \<noteq> ?c"
       have *: "0 < inverse (real n + 1)" "inverse (real n + 1) \<le> 1"
         unfolding inverse_le_1_iff by auto
       have "(inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b)) + (1 - inverse (real n + 1)) *\<^sub>R x =
         x + (inverse (real n + 1)) *\<^sub>R (((1 / 2) *\<^sub>R (a + b)) - x)"
         by (auto simp add: algebra_simps)
-      then have "f n < b" and "a < f n"
+      then have "f n <e b" and "a <e f n"
         using open_closed_interval_convex[OF open_interval_midpoint[OF assms] as *]
-        unfolding f_def by auto
+        unfolding f_def by (auto simp: interval eucl_less_def)
       then have False
         using fn unfolding f_def using xc by auto
     }
@@ -6448,11 +6451,11 @@
         using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"]
         by auto
     }
-    ultimately have "x \<in> closure {a<..<b}"
+    ultimately have "x \<in> closure (box a b)"
       using as and open_interval_midpoint[OF assms]
       unfolding closure_def
       unfolding islimpt_sequential
-      by (cases "x=?c") auto
+      by (cases "x=?c") (auto simp: in_box_eucl_less)
   }
   then show ?thesis
     using closure_minimal[OF interval_open_subset_closed closed_interval, of a b] by blast
@@ -6461,7 +6464,7 @@
 lemma bounded_subset_open_interval_symmetric:
   fixes s::"('a::ordered_euclidean_space) set"
   assumes "bounded s"
-  shows "\<exists>a. s \<subseteq> {-a<..<a}"
+  shows "\<exists>a. s \<subseteq> box (-a) a"
 proof -
   obtain b where "b>0" and b: "\<forall>x\<in>s. norm x \<le> b"
     using assms[unfolded bounded_pos] by auto
@@ -6478,12 +6481,12 @@
       by auto
   }
   then show ?thesis
-    by (auto intro: exI[where x=a] simp add: eucl_less[where 'a='a])
+    by (auto intro: exI[where x=a] simp add: interval)
 qed
 
 lemma bounded_subset_open_interval:
   fixes s :: "('a::ordered_euclidean_space) set"
-  shows "bounded s \<Longrightarrow> (\<exists>a b. s \<subseteq> {a<..<b})"
+  shows "bounded s \<Longrightarrow> (\<exists>a b. s \<subseteq> box a b)"
   by (auto dest!: bounded_subset_open_interval_symmetric)
 
 lemma bounded_subset_closed_interval_symmetric:
@@ -6491,7 +6494,7 @@
   assumes "bounded s"
   shows "\<exists>a. s \<subseteq> {-a .. a}"
 proof -
-  obtain a where "s \<subseteq> {- a<..<a}"
+  obtain a where "s \<subseteq> box (-a) a"
     using bounded_subset_open_interval_symmetric[OF assms] by auto
   then show ?thesis
     using interval_open_subset_closed[of "-a" a] by auto
@@ -6504,13 +6507,13 @@
 
 lemma frontier_closed_interval:
   fixes a b :: "'a::ordered_euclidean_space"
-  shows "frontier {a .. b} = {a .. b} - {a<..<b}"
+  shows "frontier {a .. b} = {a .. b} - box a b"
   unfolding frontier_def unfolding interior_closed_interval and closure_closed[OF closed_interval] ..
 
 lemma frontier_open_interval:
   fixes a b :: "'a::ordered_euclidean_space"
-  shows "frontier {a<..<b} = (if {a<..<b} = {} then {} else {a .. b} - {a<..<b})"
-proof (cases "{a<..<b} = {}")
+  shows "frontier (box a b) = (if box a b = {} then {} else {a .. b} - box a b)"
+proof (cases "box a b = {}")
   case True
   then show ?thesis
     using frontier_empty by auto
@@ -6523,8 +6526,8 @@
 
 lemma inter_interval_mixed_eq_empty:
   fixes a :: "'a::ordered_euclidean_space"
-  assumes "{c<..<d} \<noteq> {}"
-  shows "{a<..<b} \<inter> {c .. d} = {} \<longleftrightarrow> {a<..<b} \<inter> {c<..<d} = {}"
+  assumes "box c d \<noteq> {}"
+  shows "box a b \<inter> {c .. d} = {} \<longleftrightarrow> box a b \<inter> box c d = {}"
   unfolding closure_open_interval[OF assms, symmetric]
   unfolding open_inter_closure_eq_empty[OF open_interval] ..
 
@@ -6577,7 +6580,7 @@
   (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. ((a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i) \<or> (b\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> a\<bullet>i))) \<longrightarrow> x \<in> s)"
 
 lemma is_interval_interval: "is_interval {a .. b::'a::ordered_euclidean_space}" (is ?th1)
-  "is_interval {a<..<b}" (is ?th2) proof -
+  "is_interval (box a b)" (is ?th2) proof -
   show ?th1 ?th2  unfolding is_interval_def mem_interval Ball_def atLeastAtMost_iff
     by(meson order_trans le_less_trans less_le_trans less_trans)+ qed
 
@@ -6705,13 +6708,13 @@
 
 lemma eucl_lessThan_eq_halfspaces:
   fixes a :: "'a\<Colon>ordered_euclidean_space"
-  shows "{..<a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
-  by (auto simp: eucl_less[where 'a='a])
+  shows "{x. x <e a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
+  by (auto simp: eucl_less_def)
 
 lemma eucl_greaterThan_eq_halfspaces:
   fixes a :: "'a\<Colon>ordered_euclidean_space"
-  shows "{a<..} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
-  by (auto simp: eucl_less[where 'a='a])
+  shows "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
+  by (auto simp: eucl_less_def)
 
 lemma eucl_atMost_eq_halfspaces:
   fixes a :: "'a\<Colon>ordered_euclidean_space"
@@ -6725,12 +6728,12 @@
 
 lemma open_eucl_lessThan[simp, intro]:
   fixes a :: "'a\<Colon>ordered_euclidean_space"
-  shows "open {..< a}"
+  shows "open {x. x <e a}"
   by (auto simp: eucl_lessThan_eq_halfspaces open_halfspace_component_lt)
 
 lemma open_eucl_greaterThan[simp, intro]:
   fixes a :: "'a\<Colon>ordered_euclidean_space"
-  shows "open {a <..}"
+  shows "open {x. a <e x}"
   by (auto simp: eucl_greaterThan_eq_halfspaces open_halfspace_component_gt)
 
 lemma closed_eucl_atMost[simp, intro]:
@@ -7101,7 +7104,7 @@
       by auto
     then obtain l where "l\<in>s" and l:"(x ---> l) sequentially"
       using cs[unfolded complete_def, THEN spec[where x="x"]]
-      using cauchy_isometric[OF `0<e` s f normf] and cfg and x(1)
+      using cauchy_isometric[OF `0 < e` s f normf] and cfg and x(1)
       by auto
     then have "\<exists>l\<in>f ` s. (g ---> l) sequentially"
       using linear_continuous_at[OF f, unfolded continuous_at_sequentially, THEN spec[where x=x], of l]
@@ -7628,4 +7631,7 @@
 
 declare tendsto_const [intro] (* FIXME: move *)
 
+no_notation
+  eucl_less (infix "<e" 50)
+
 end
diff -r 81290fe85890 -r 2d3df8633dad src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Mon Dec 16 14:49:18 2013 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Mon Dec 16 17:08:22 2013 +0100
@@ -237,18 +237,25 @@
   by (blast intro: borel_open borel_closed open_lessThan open_greaterThan open_greaterThanLessThan
                    closed_atMost closed_atLeast closed_atLeastAtMost)+
 
+notation
+  eucl_less (infix "<e" 50)
+
+lemma box_oc: "{x. a <e x \<and> x \<le> b} = {x. a <e x} \<inter> {..b}"
+  and box_co: "{x. a \<le> x \<and> x <e b} = {a..} \<inter> {x. x <e b}"
+  by auto
+
 lemma eucl_ivals[measurable]:
   fixes a b :: "'a\<Colon>ordered_euclidean_space"
-  shows "{..< a} \<in> sets borel"
-    and "{a <..} \<in> sets borel"
-    and "{a<..<b} \<in> sets borel"
+  shows "{x. x <e a} \<in> sets borel"
+    and "{x. a <e x} \<in> sets borel"
+    and "box a b \<in> sets borel"
     and "{..a} \<in> sets borel"
     and "{a..} \<in> sets borel"
     and "{a..b} \<in> sets borel"
-    and  "{a<..b} \<in> sets borel"
-    and "{a..<b} \<in> sets borel"
-  unfolding greaterThanAtMost_def atLeastLessThan_def
-  by (blast intro: borel_open borel_closed)+
+    and  "{x. a <e x \<and> x \<le> b} \<in> sets borel"
+    and "{x. a \<le> x \<and>  x <e b} \<in> sets borel"
+  unfolding box_oc box_co
+  by (auto intro: borel_open borel_closed)
 
 lemma open_Collect_less:
   fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}"
@@ -375,11 +382,6 @@
     done
 qed (auto simp: box_def)
 
-lemma borel_eq_greaterThanLessThan:
-  "borel = sigma UNIV (range (\<lambda> (a, b). {a <..< b} :: 'a \<Colon> ordered_euclidean_space set))"
-  unfolding borel_eq_box apply (rule arg_cong2[where f=sigma])
-  by (auto simp: box_def image_iff mem_interval set_eq_iff simp del: greaterThanLessThan_iff)
-
 lemma halfspace_gt_in_halfspace:
   assumes i: "i \<in> A"
   shows "{x\<Colon>'a. a < x \<bullet> i} \<in> 
@@ -484,15 +486,15 @@
 qed auto
 
 lemma borel_eq_greaterThan:
-  "borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {a<..}))"
+  "borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {x. a <e x}))"
   (is "_ = ?SIGMA")
 proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_le])
   fix a :: real and i :: 'a assume "(a, i) \<in> UNIV \<times> Basis"
   then have i: "i \<in> Basis" by auto
   have "{x::'a. x\<bullet>i \<le> a} = UNIV - {x::'a. a < x\<bullet>i}" by auto
   also have *: "{x::'a. a < x\<bullet>i} =
-      (\<Union>k::nat. {\<Sum>n\<in>Basis. (if n = i then a else -real k) *\<^sub>R n <..})" using i
-  proof (safe, simp_all add: eucl_less[where 'a='a] split: split_if_asm)
+      (\<Union>k::nat. {x. (\<Sum>n\<in>Basis. (if n = i then a else -real k) *\<^sub>R n) <e x})" using i
+  proof (safe, simp_all add: eucl_less_def split: split_if_asm)
     fix x :: 'a
     from reals_Archimedean2[of "Max ((\<lambda>i. -x\<bullet>i)`Basis)"]
     guess k::nat .. note k = this
@@ -511,14 +513,14 @@
 qed auto
 
 lemma borel_eq_lessThan:
-  "borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {..<a}))"
+  "borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {x. x <e a}))"
   (is "_ = ?SIGMA")
 proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_ge])
   fix a :: real and i :: 'a assume "(a, i) \<in> UNIV \<times> Basis"
   then have i: "i \<in> Basis" by auto
   have "{x::'a. a \<le> x\<bullet>i} = UNIV - {x::'a. x\<bullet>i < a}" by auto
-  also have *: "{x::'a. x\<bullet>i < a} = (\<Union>k::nat. {..< \<Sum>n\<in>Basis. (if n = i then a else real k) *\<^sub>R n})" using `i\<in> Basis`
-  proof (safe, simp_all add: eucl_less[where 'a='a] split: split_if_asm)
+  also have *: "{x::'a. x\<bullet>i < a} = (\<Union>k::nat. {x. x <e (\<Sum>n\<in>Basis. (if n = i then a else real k) *\<^sub>R n)})" using `i\<in> Basis`
+  proof (safe, simp_all add: eucl_less_def split: split_if_asm)
     fix x :: 'a
     from reals_Archimedean2[of "Max ((\<lambda>i. x\<bullet>i)`Basis)"]
     guess k::nat .. note k = this
@@ -532,7 +534,7 @@
   finally show "{x. a \<le> x\<bullet>i} \<in> ?SIGMA"
     apply (simp only:)
     apply (safe intro!: sets.countable_UN sets.Diff)
-    apply (auto intro: sigma_sets_top)
+    apply (auto intro: sigma_sets_top )
     done
 qed auto
 
@@ -558,6 +560,9 @@
        (auto intro!: sigma_sets_top)
 qed auto
 
+lemma eucl_lessThan: "{x::real. x <e a} = lessThan a"
+  by (simp add: eucl_less_def lessThan_def)
+
 lemma borel_eq_atLeastLessThan:
   "borel = sigma UNIV (range (\<lambda>(a, b). {a ..< b :: real}))" (is "_ = ?SIGMA")
 proof (rule borel_eq_sigmaI5[OF borel_eq_lessThan])
@@ -565,8 +570,8 @@
   fix x :: real
   have "{..<x} = (\<Union>i::nat. {-real i ..< x})"
     by (auto simp: move_uminus real_arch_simple)
-  then show "{..< x} \<in> ?SIGMA"
-    by (auto intro: sigma_sets.intros)
+  then show "{y. y <e x} \<in> ?SIGMA"
+    by (auto intro: sigma_sets.intros simp: eucl_lessThan)
 qed auto
 
 lemma borel_eq_closed: "borel = sigma UNIV (Collect closed)"
@@ -1195,4 +1200,7 @@
   shows "(\<lambda>x. suminf (\<lambda>i. f i x)) \<in> borel_measurable M"
   unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
 
+no_notation
+  eucl_less (infix "<e" 50)
+
 end
diff -r 81290fe85890 -r 2d3df8633dad src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Mon Dec 16 14:49:18 2013 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Mon Dec 16 17:08:22 2013 +0100
@@ -916,16 +916,15 @@
 proof (subst sigma_prod_algebra_sigma_eq[where S="\<lambda>_ i::nat. {..<real i}" and E="\<lambda>_. range lessThan", OF I])
   show "sigma_sets (space (Pi\<^sub>M I (\<lambda>i. lborel))) {Pi\<^sub>E I F |F. \<forall>i\<in>I. F i \<in> range lessThan} = ?G"
     by (intro arg_cong2[where f=sigma_sets]) (auto simp: space_PiM image_iff bchoice_iff)
-qed (auto simp: borel_eq_lessThan reals_Archimedean2)
+qed (auto simp: borel_eq_lessThan eucl_lessThan reals_Archimedean2)
 
 lemma measurable_e2p[measurable]:
   "e2p \<in> measurable (borel::'a::ordered_euclidean_space measure) (\<Pi>\<^sub>M (i::'a)\<in>Basis. (lborel :: real measure))"
 proof (rule measurable_sigma_sets[OF sets_product_borel])
   fix A :: "('a \<Rightarrow> real) set" assume "A \<in> {\<Pi>\<^sub>E (i::'a)\<in>Basis. {..<x i} |x. True} "
   then obtain x where  "A = (\<Pi>\<^sub>E (i::'a)\<in>Basis. {..<x i})" by auto
-  then have "e2p -` A = {..< (\<Sum>i\<in>Basis. x i *\<^sub>R i) :: 'a}"
-    using DIM_positive by (auto simp add: set_eq_iff e2p_def
-      euclidean_eq_iff[where 'a='a] eucl_less[where 'a='a])
+  then have "e2p -` A = {y :: 'a. eucl_less y (\<Sum>i\<in>Basis. x i *\<^sub>R i)}"
+    using DIM_positive by (auto simp add: set_eq_iff e2p_def eucl_less_def)
   then show "e2p -` A \<inter> space (borel::'a measure) \<in> sets borel" by simp
 qed (auto simp: e2p_def)