# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1502734627 -3600
# Node ID 2891f33ed4c8331d3c7d72dd22731c674ba654cd
# Parent  7fa0b300fb0dbdbca23fd965c52b4dddd4b11eb0
patching the previous commit

diff -r 7fa0b300fb0d -r 2891f33ed4c8 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- 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
 
diff -r 7fa0b300fb0d -r 2891f33ed4c8 src/HOL/Real_Vector_Spaces.thy
--- 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"