diff -r dbc62f86a1a9 -r de25474ce728 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Tue Mar 15 14:08:25 2016 +0000
+++ b/src/HOL/Real.thy	Wed Mar 16 13:57:06 2016 +0000
@@ -1404,21 +1404,6 @@
 lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
   by simp
 
-subsection\<open>Absolute Value Function for the Reals\<close>
-
-lemma abs_minus_add_cancel: "\<bar>x + (- y)\<bar> = \<bar>y + (- (x::real))\<bar>"
-  by (simp add: abs_if)
-
-lemma abs_add_one_gt_zero: "(0::real) < 1 + \<bar>x\<bar>"
-  by (simp add: abs_if)
-
-lemma abs_add_one_not_less_self: "~ \<bar>x\<bar> + (1::real) < x"
-  by simp
-
-lemma abs_sum_triangle_ineq: "\<bar>(x::real) + y + (-l + -m)\<bar> \<le> \<bar>x + -l\<bar> + \<bar>y + -m\<bar>"
-  by simp
-
-
 subsection\<open>Floor and Ceiling Functions from the Reals to the Integers\<close>
 
 (* FIXME: theorems for negative numerals. Many duplicates, e.g. from Archimedean_Field.thy. *)
@@ -1564,7 +1549,7 @@
 proof -
   have "x ^ n = of_int (\<lfloor>x\<rfloor> ^ n)"
     using assms by (induct n arbitrary: x) simp_all
-  then show ?thesis by (metis floor_of_int) 
+  then show ?thesis by (metis floor_of_int)
 qed
 
 lemma floor_numeral_power[simp]: