src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy

       also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi"
         by (simp only: ya)
       also from y1 y2 have "h (y1 + y2) = h y1 + h y2"
         by simp
       also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
-        by (simp add: real_add_mult_distrib)
+        by (simp add: left_distrib)
       also from h'_def x1_rep _ HE y1 x0
       have "h y1 + a1 * xi = h' x1"
         by (rule h'_definite [symmetric])
       also from h'_def x2_rep _ HE y2 x0
       have "h y2 + a2 * xi = h' x2"

       also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi"
         by (simp only: ya)
       also from y1 have "h (c \<cdot> y1) = c * h y1"
         by simp
       also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)"
-        by (simp only: real_add_mult_distrib2)
+        by (simp only: right_distrib)
       also from h'_def x1_rep _ HE y1 x0 have "h y1 + a1 * xi = h' x1"
         by (rule h'_definite [symmetric])
       finally show ?thesis .
     qed
   }