# HG changeset patch
# User wenzelm
# Date 1419877044 -3600
# Node ID c112a24446d473fb9896eb00b8bbfdeb6e5ff317
# Parent  73a6403637b343d79d842b233ad9131210580994
tuned whitespace;

diff -r 73a6403637b3 -r c112a24446d4 src/HOL/Hahn_Banach/Hahn_Banach.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Mon Dec 29 15:38:59 2014 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Mon Dec 29 19:17:24 2014 +0100
@@ -297,7 +297,7 @@
 qed
 
 
-subsection  \<open>Alternative formulation\<close>
+subsection \<open>Alternative formulation\<close>
 
 text \<open>
   The following alternative formulation of the Hahn-Banach