# HG changeset patch
# User wenzelm
# Date 1489090652 -3600
# Node ID f8aafbf2b02ecc1bc05412daeaa8f72eeb8e66b8
# Parent  d98ede9e59173372df0d82fc620d815cb2f2e327
tuned;

diff -r d98ede9e5917 -r f8aafbf2b02e src/HOL/Hahn_Banach/Hahn_Banach.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Thu Mar 09 21:09:45 2017 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Thu Mar 09 21:17:32 2017 +0100
@@ -475,8 +475,7 @@
       proof -
         from a x have "g x = f x" ..
         then have "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:)
-        also from g_cont
-        have "\<dots> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
+        also from g_cont have "\<dots> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
         proof (rule fn_norm_le_cong [OF _ linearformE, folded B_def fn_norm_def])
           from FE x show "x \<in> E" ..
         qed
@@ -484,8 +483,7 @@
       qed
     next
       show "0 \<le> \<parallel>g\<parallel>\<hyphen>E"
-        using g_cont
-        by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def])
+        using g_cont by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def])
       show "continuous F f norm" by fact
     qed
   qed