# HG changeset patch
# User wenzelm
# Date 1446476552 -3600
# Node ID de44d4fa5ef0cdda25d98db9a682758903617bde
# Parent b3eb789616c37f533a945f57198b68d5a1b2943b
tuned whitespace;
diff -r b3eb789616c3 -r de44d4fa5ef0 src/HOL/Hahn_Banach/Hahn_Banach.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy Mon Nov 02 14:09:14 2015 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy Mon Nov 02 16:02:32 2015 +0100
@@ -22,7 +22,8 @@
on \E\, and \f\ be a linear form defined on \F\ such that \f\ is bounded
by \p\, i.e. \\x \ F. f x \ p x\. Then \f\ can be extended to a linear
form \h\ on \E\ such that \h\ is norm-preserving, i.e. \h\ is also bounded
- by \p\. \
+ by \p\.
+\
paragraph \Proof Sketch.\
text \