--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Mon Aug 14 18:54:51 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Mon Aug 14 19:17:07 2017 +0100
@@ -9,23 +9,6 @@
Lebesgue_Measure Tagged_Division
begin
-(*MOVE ALL THESE*)
-lemma abs_triangle_half_r:
- fixes y :: "'a::linordered_field"
- shows "abs (y - x1) < e / 2 \<Longrightarrow> abs (y - x2) < e / 2 \<Longrightarrow> abs (x1 - x2) < e"
- by linarith
-
-lemma abs_triangle_half_l:
- fixes y :: "'a::linordered_field"
- assumes "abs (x - y) < e / 2"
- and "abs (x' - y) < e / 2"
- shows "abs (x - x') < e"
- using assms by linarith
-
-lemma eps_leI:
- assumes "(\<And>e::'a::linordered_idom. 0 < e \<Longrightarrow> x < y + e)" shows "x \<le> y"
- by (metis add_diff_eq assms diff_diff_add diff_gt_0_iff_gt linorder_not_less order_less_irrefl)
-
(*FIXME DELETE*)
lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
--- a/src/HOL/Real_Vector_Spaces.thy Mon Aug 14 18:54:51 2017 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Mon Aug 14 19:17:07 2017 +0100
@@ -825,8 +825,10 @@
then show ?thesis by simp
qed
-lemma norm_triangle_le_diff: "norm x + norm y \<le> e \<Longrightarrow> norm (x - y) \<le> e"
- by (meson norm_triangle_ineq4 order_trans)
+lemma norm_triangle_le_diff:
+ fixes x y :: "'a::real_normed_vector"
+ shows "norm x + norm y \<le> e \<Longrightarrow> norm (x - y) \<le> e"
+ by (meson norm_triangle_ineq4 order_trans)
lemma norm_diff_ineq: "norm a - norm b \<le> norm (a + b)"
for a b :: "'a::real_normed_vector"