# HG changeset patch
# User wenzelm
# Date 1449497788 -3600
# Node ID f3789d5b96caef00b3247781a5e66d336be0836b
# Parent  4cf66f21b764ee433875f9829ffe965a6ddc0165
tuned whitespace;

diff -r 4cf66f21b764 -r f3789d5b96ca src/HOL/Hahn_Banach/Hahn_Banach.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Mon Dec 07 15:16:28 2015 +0100
@@ -189,7 +189,7 @@
       proof
         show "g \<subseteq> graph H' h'"
         proof -
-          have  "graph H h \<subseteq> graph H' h'"
+          have "graph H h \<subseteq> graph H' h'"
           proof (rule graph_extI)
             fix t assume t: "t \<in> H"
             from E HE t have "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)"