src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy

     Author:     Gertrud Bauer, TU Munich
 *)
 
 header {* Extending non-maximal functions *}
 
-theory HahnBanachExtLemmas = FunctionNorm + RealLemmas:
+theory HahnBanachExtLemmas = FunctionNorm:
 
 text {*
   In this section the following context is presumed.  Let @{text E} be
   a real vector space with a seminorm @{text q} on @{text E}. @{text
   F} is a subspace of @{text E} and @{text f} a linear function on

           a * (- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
         by (simp add: mult_left_mono_neg order_less_imp_le)
 
       also have "\<dots> =
           - a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))"
-	by (rule real_mult_diff_distrib) 
+	by (simp add: right_diff_distrib)
       also from lz x0 y' have "- a * (p (inverse a \<cdot> y + x0)) =
           p (a \<cdot> (inverse a \<cdot> y + x0))"
         by (simp add: abs_homogenous abs_minus_eqI2)
       also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
         by (simp add: add_mult_distrib1 mult_assoc [symmetric])

       have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" ..
       with gz have "a * xi \<le>
           a * (p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
         by simp
       also have "... = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"
-	by (rule real_mult_diff_distrib2) 
+	by (simp add: right_diff_distrib)
       also from gz x0 y'
       have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"
         by (simp add: abs_homogenous abs_eqI2)
       also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
         by (simp add: add_mult_distrib1 mult_assoc [symmetric])