tuned;

--- a/src/HOL/Real/HahnBanach/Aux.thy	Wed Aug 09 11:53:00 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Aux.thy	Wed Aug 09 17:10:41 2000 +0200
@@ -103,7 +103,7 @@
   thus ?thesis by simp
 qed
 
-lemma real_mult_inv_right1: "x \<noteq> #0 ==> x*rinv(x) = #1"
+lemma real_mult_inv_right1: "x \<noteq> #0 ==> x * rinv(x) = #1"
   by simp
 
 lemma real_mult_inv_left1: "x \<noteq> #0 ==> rinv(x) * x = #1"

--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Wed Aug 09 11:53:00 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Wed Aug 09 17:10:41 2000 +0200
@@ -167,7 +167,7 @@
         qed blast
         def H' == "H + lin x'"
         -- {* Define $H'$ as the direct sum of $H$ and the linear closure of $x'$. \skp *}
-        obtain xi where "\<forall>y \<in> H. - p (y + x') - h y <= xi 
+        obtain xi where "\<forall>y \<in> H. - p (y + x') - h y <= xi  
                           \<and> xi <= p (y + x') - h y" 
         -- {* Pick a real number $\xi$ that fulfills certain inequations; this will *}
         -- {* be used to establish that $h'$ is a norm-preserving extension of $h$. 
@@ -198,7 +198,7 @@
         qed
 
         def h' == "\<lambda>x. let (y,a) = SOME (y,a). x = y + a \<cdot> x' \<and> y \<in> H
-                       in (h y) + a * xi"
+                       in h y + a * xi"
         -- {* Define the extension $h'$ of $h$ to $H'$ using $\xi$. \skp *}
         show ?thesis
         proof