diff -r d01983034ded -r 247615bfffb8 src/HOL/Real/HahnBanach/FunctionNorm.thy
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Thu May 06 20:43:30 2004 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Fri May 07 12:16:57 2004 +0200
@@ -137,7 +137,7 @@
             by (rule real_mult_assoc)
           also
           from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp
-          hence "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by (simp add: real_mult_inv_right1)
+          hence "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by simp 
           also have "c * 1 \<le> b" by (simp add: b_def le_maxI1)
           finally show "y \<le> b" .
         qed
@@ -199,13 +199,11 @@
   then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp
   also have "f 0 = 0" ..
   also have "\<bar>\<dots>\<bar> = 0" by simp
-  also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
-  proof (rule real_le_mult_order1a)
-    show "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
+  also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
       by (unfold B_def fn_norm_def)
         (rule fn_norm_ge_zero [OF _ continuous.intro])
-    show "0 \<le> norm x" ..
-  qed
+    have "0 \<le> norm x" ..
+  with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff)
   finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
 next
   assume "x \<noteq> 0"