--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Mon Dec 29 06:49:26 2003 +0100
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Thu Jan 01 10:06:32 2004 +0100
@@ -134,7 +134,7 @@
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])
@@ -173,7 +173,7 @@
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 .