Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned whitespace;
authorwenzelm
Mon, 07 Dec 2015 15:16:28 +0100
changeset 61800 f3789d5b96ca
parent 61799 4cf66f21b764
child 61801 fa8d1cdf6518
tuned whitespace;
src/HOL/Hahn_Banach/Hahn_Banach.thy file | annotate | diff | comparison | revisions 
--- 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)"
isabelle