diff -r f5ca4c2157a5 -r 2f4e2aab190a src/HOL/Real.thy
--- a/src/HOL/Real.thy	Thu Jun 28 10:13:54 2018 +0200
+++ b/src/HOL/Real.thy	Thu Jun 28 14:13:57 2018 +0100
@@ -1383,21 +1383,16 @@
 
 subsection \<open>Density of the Reals\<close>
 
-lemma real_lbound_gt_zero: "0 < d1 \<Longrightarrow> 0 < d2 \<Longrightarrow> \<exists>e. 0 < e \<and> e < d1 \<and> e < d2"
-  for d1 d2 :: real
+lemma field_lbound_gt_zero: "0 < d1 \<Longrightarrow> 0 < d2 \<Longrightarrow> \<exists>e. 0 < e \<and> e < d1 \<and> e < d2"
+  for d1 d2 :: "'a::linordered_field"
   by (rule exI [where x = "min d1 d2 / 2"]) (simp add: min_def)
 
-text \<open>Similar results are proved in @{theory HOL.Fields}\<close>
-lemma real_less_half_sum: "x < y \<Longrightarrow> x < (x + y) / 2"
-  for x y :: real
+lemma field_less_half_sum: "x < y \<Longrightarrow> x < (x + y) / 2"
+  for x y :: "'a::linordered_field"
   by auto
 
-lemma real_gt_half_sum: "x < y \<Longrightarrow> (x + y) / 2 < y"
-  for x y :: real
-  by auto
-
-lemma real_sum_of_halves: "x / 2 + x / 2 = x"
-  for x :: real
+lemma field_sum_of_halves: "x / 2 + x / 2 = x"
+  for x :: "'a::linordered_field"
   by simp