# HG changeset patch
# User wenzelm
# Date 1446460982 -3600
# Node ID f92bf6674699fce4ae45c65c5aafd499488c2649
# Parent  a29295dac1ca8425b072bfd03bef59405d0d39c9
tuned document;

diff -r a29295dac1ca -r f92bf6674699 src/HOL/Hahn_Banach/Function_Norm.thy
--- a/src/HOL/Hahn_Banach/Function_Norm.thy	Mon Nov 02 11:10:28 2015 +0100
+++ b/src/HOL/Hahn_Banach/Function_Norm.thy	Mon Nov 02 11:43:02 2015 +0100
@@ -11,14 +11,13 @@
 subsection \<open>Continuous linear forms\<close>
 
 text \<open>
-  A linear form \<open>f\<close> on a normed vector space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close>
-  is \<^emph>\<open>continuous\<close>, iff it is bounded, i.e.
+  A linear form \<open>f\<close> on a normed vector space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> is \<^emph>\<open>continuous\<close>,
+  iff it is bounded, i.e.
   \begin{center}
   \<open>\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
   \end{center}
-  In our application no other functions than linear forms are
-  considered, so we can define continuous linear forms as bounded
-  linear forms:
+  In our application no other functions than linear forms are considered, so
+  we can define continuous linear forms as bounded linear forms:
 \<close>
 
 locale continuous = linearform +
@@ -48,28 +47,25 @@
   \end{center}
   is called the \<^emph>\<open>norm\<close> of \<open>f\<close>.
 
-  For non-trivial vector spaces \<open>V \<noteq> {0}\<close> the norm can be
-  defined as
+  For non-trivial vector spaces \<open>V \<noteq> {0}\<close> the norm can be defined as
   \begin{center}
   \<open>\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>\<close>
   \end{center}
 
-  For the case \<open>V = {0}\<close> the supremum would be taken from an
-  empty set. Since \<open>\<real>\<close> is unbounded, there would be no supremum.
-  To avoid this situation it must be guaranteed that there is an
-  element in this set. This element must be \<open>{} \<ge> 0\<close> so that
-  \<open>fn_norm\<close> has the norm properties. Furthermore it does not
-  have to change the norm in all other cases, so it must be \<open>0\<close>,
-  as all other elements are \<open>{} \<ge> 0\<close>.
+  For the case \<open>V = {0}\<close> the supremum would be taken from an empty set.
+  Since \<open>\<real>\<close> is unbounded, there would be no supremum. To avoid this
+  situation it must be guaranteed that there is an element in this set. This
+  element must be \<open>{} \<ge> 0\<close> so that \<open>fn_norm\<close> has the norm properties.
+  Furthermore it does not have to change the norm in all other cases, so it
+  must be \<open>0\<close>, as all other elements are \<open>{} \<ge> 0\<close>.
 
-  Thus we define the set \<open>B\<close> where the supremum is taken from as
-  follows:
+  Thus we define the set \<open>B\<close> where the supremum is taken from as follows:
   \begin{center}
   \<open>{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}\<close>
   \end{center}
 
-  \<open>fn_norm\<close> is equal to the supremum of \<open>B\<close>, if the
-  supremum exists (otherwise it is undefined).
+  \<open>fn_norm\<close> is equal to the supremum of \<open>B\<close>, if the supremum exists
+  (otherwise it is undefined).
 \<close>
 
 locale fn_norm =
@@ -84,8 +80,8 @@
   by (simp add: B_def)
 
 text \<open>
-  The following lemma states that every continuous linear form on a
-  normed space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> has a function norm.
+  The following lemma states that every continuous linear form on a normed
+  space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> has a function norm.
 \<close>
 
 lemma (in normed_vectorspace_with_fn_norm) fn_norm_works:
@@ -108,9 +104,9 @@
       txt \<open>We know that \<open>f\<close> is bounded by some value \<open>c\<close>.\<close>
       from bounded obtain c where c: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
 
-      txt \<open>To prove the thesis, we have to show that there is some
-        \<open>b\<close>, such that \<open>y \<le> b\<close> for all \<open>y \<in>
-        B\<close>. Due to the definition of \<open>B\<close> there are two cases.\<close>
+      txt \<open>To prove the thesis, we have to show that there is some \<open>b\<close>, such
+        that \<open>y \<le> b\<close> for all \<open>y \<in> B\<close>. Due to the definition of \<open>B\<close> there are
+        two cases.\<close>
 
       def b \<equiv> "max c 0"
       have "\<forall>y \<in> B V f. y \<le> b"
@@ -237,8 +233,8 @@
 
 text \<open>
   \<^medskip>
-  The function norm is the least positive real number for
-  which the following inequation holds:
+  The function norm is the least positive real number for which the
+  following inequality holds:
   \begin{center}
     \<open>\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
   \end{center}
diff -r a29295dac1ca -r f92bf6674699 src/HOL/Hahn_Banach/Function_Order.thy
--- a/src/HOL/Hahn_Banach/Function_Order.thy	Mon Nov 02 11:10:28 2015 +0100
+++ b/src/HOL/Hahn_Banach/Function_Order.thy	Mon Nov 02 11:43:02 2015 +0100
@@ -70,8 +70,8 @@
   where "funct g = (\<lambda>x. (SOME y. (x, y) \<in> g))"
 
 text \<open>
-  The following lemma states that \<open>g\<close> is the graph of a function
-  if the relation induced by \<open>g\<close> is unique.
+  The following lemma states that \<open>g\<close> is the graph of a function if the
+  relation induced by \<open>g\<close> is unique.
 \<close>
 
 lemma graph_domain_funct:
@@ -93,9 +93,9 @@
 subsection \<open>Norm-preserving extensions of a function\<close>
 
 text \<open>
-  Given a linear form \<open>f\<close> on the space \<open>F\<close> and a seminorm
-  \<open>p\<close> on \<open>E\<close>. The set of all linear extensions of \<open>f\<close>, to superspaces \<open>H\<close> of \<open>F\<close>, which are bounded by
-  \<open>p\<close>, is defined as follows.
+  Given a linear form \<open>f\<close> on the space \<open>F\<close> and a seminorm \<open>p\<close> on \<open>E\<close>. The
+  set of all linear extensions of \<open>f\<close>, to superspaces \<open>H\<close> of \<open>F\<close>, which are
+  bounded by \<open>p\<close>, is defined as follows.
 \<close>
 
 definition
diff -r a29295dac1ca -r f92bf6674699 src/HOL/Hahn_Banach/Hahn_Banach.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Mon Nov 02 11:10:28 2015 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Mon Nov 02 11:43:02 2015 +0100
@@ -9,37 +9,36 @@
 begin
 
 text \<open>
-  We present the proof of two different versions of the Hahn-Banach
-  Theorem, closely following @{cite \<open>\S36\<close> "Heuser:1986"}.
+  We present the proof of two different versions of the Hahn-Banach Theorem,
+  closely following @{cite \<open>\S36\<close> "Heuser:1986"}.
 \<close>
 
+
 subsection \<open>The Hahn-Banach Theorem for vector spaces\<close>
 
 paragraph \<open>Hahn-Banach Theorem.\<close>
 text \<open>
-  Let \<open>F\<close> be a subspace of a real vector space \<open>E\<close>, let \<open>p\<close> be a semi-norm on \<open>E\<close>, and \<open>f\<close> be a linear form defined on
-  \<open>F\<close> such that \<open>f\<close> is bounded by \<open>p\<close>, i.e. \<open>\<forall>x \<in>
-  F. f x \<le> p x\<close>. Then \<open>f\<close> can be extended to a linear form \<open>h\<close>
-  on \<open>E\<close> such that \<open>h\<close> is norm-preserving, i.e. \<open>h\<close> is
-  also bounded by \<open>p\<close>.
-\<close>
+  Let \<open>F\<close> be a subspace of a real vector space \<open>E\<close>, let \<open>p\<close> be a semi-norm
+  on \<open>E\<close>, and \<open>f\<close> be a linear form defined on \<open>F\<close> such that \<open>f\<close> is bounded
+  by \<open>p\<close>, i.e. \<open>\<forall>x \<in> F. f x \<le> p x\<close>. Then \<open>f\<close> can be extended to a linear
+  form \<open>h\<close> on \<open>E\<close> such that \<open>h\<close> is norm-preserving, i.e. \<open>h\<close> is also bounded
+  by \<open>p\<close>. \<close>
 
 paragraph \<open>Proof Sketch.\<close>
 text \<open>
-  \<^enum> Define \<open>M\<close> as the set of norm-preserving extensions of
-  \<open>f\<close> to subspaces of \<open>E\<close>. The linear forms in \<open>M\<close>
-  are ordered by domain extension.
+  \<^enum> Define \<open>M\<close> as the set of norm-preserving extensions of \<open>f\<close> to subspaces
+  of \<open>E\<close>. The linear forms in \<open>M\<close> are ordered by domain extension.
 
-  \<^enum> We show that every non-empty chain in \<open>M\<close> has an upper
-  bound in \<open>M\<close>.
+  \<^enum> We show that every non-empty chain in \<open>M\<close> has an upper bound in \<open>M\<close>.
 
-  \<^enum> With Zorn's Lemma we conclude that there is a maximal function
-  \<open>g\<close> in \<open>M\<close>.
+  \<^enum> With Zorn's Lemma we conclude that there is a maximal function \<open>g\<close> in
+  \<open>M\<close>.
 
-  \<^enum> The domain \<open>H\<close> of \<open>g\<close> is the whole space \<open>E\<close>, as shown by classical contradiction:
+  \<^enum> The domain \<open>H\<close> of \<open>g\<close> is the whole space \<open>E\<close>, as shown by classical
+  contradiction:
 
-    \<^item> Assuming \<open>g\<close> is not defined on whole \<open>E\<close>, it can
-    still be extended in a norm-preserving way to a super-space \<open>H'\<close> of \<open>H\<close>.
+    \<^item> Assuming \<open>g\<close> is not defined on whole \<open>E\<close>, it can still be extended in
+    a norm-preserving way to a super-space \<open>H'\<close> of \<open>H\<close>.
 
     \<^item> Thus \<open>g\<close> can not be maximal. Contradiction!
 \<close>
@@ -153,7 +152,7 @@
       obtain xi where
         xi: "\<forall>y \<in> H. - p (y + x') - h y \<le> xi
           \<and> xi \<le> p (y + x') - h y"
-        -- \<open>Pick a real number \<open>\<xi>\<close> that fulfills certain inequations; this will\<close>
+        -- \<open>Pick a real number \<open>\<xi>\<close> that fulfills certain inequality; this will\<close>
         -- \<open>be used to establish that \<open>h'\<close> is a norm-preserving extension of \<open>h\<close>.
            \label{ex-xi-use}\<^smallskip>\<close>
       proof -
@@ -292,10 +291,10 @@
 
 text \<open>
   The following alternative formulation of the Hahn-Banach
-  Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear
-  form \<open>f\<close> and a seminorm \<open>p\<close> the following inequations
-  are equivalent:\footnote{This was shown in lemma @{thm [source]
-  abs_ineq_iff} (see page \pageref{abs-ineq-iff}).}
+  Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear form
+  \<open>f\<close> and a seminorm \<open>p\<close> the following inequality are
+  equivalent:\footnote{This was shown in lemma @{thm [source] abs_ineq_iff}
+  (see page \pageref{abs-ineq-iff}).}
   \begin{center}
   \begin{tabular}{lll}
   \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and &
@@ -336,9 +335,9 @@
 subsection \<open>The Hahn-Banach Theorem for normed spaces\<close>
 
 text \<open>
-  Every continuous linear form \<open>f\<close> on a subspace \<open>F\<close> of a
-  norm space \<open>E\<close>, can be extended to a continuous linear form
-  \<open>g\<close> on \<open>E\<close> such that \<open>\<parallel>f\<parallel> = \<parallel>g\<parallel>\<close>.
+  Every continuous linear form \<open>f\<close> on a subspace \<open>F\<close> of a norm space \<open>E\<close>,
+  can be extended to a continuous linear form \<open>g\<close> on \<open>E\<close> such that \<open>\<parallel>f\<parallel> =
+  \<parallel>g\<parallel>\<close>.
 \<close>
 
 theorem norm_Hahn_Banach:
@@ -420,10 +419,10 @@
          OF F_norm, folded B_def fn_norm_def])
   qed
 
-  txt \<open>Using the fact that \<open>p\<close> is a seminorm and \<open>f\<close> is bounded
-    by \<open>p\<close> we can apply the Hahn-Banach Theorem for real vector
-    spaces. So \<open>f\<close> can be extended in a norm-preserving way to
-    some function \<open>g\<close> on the whole vector space \<open>E\<close>.\<close>
+  txt \<open>Using the fact that \<open>p\<close> is a seminorm and \<open>f\<close> is bounded by \<open>p\<close> we
+    can apply the Hahn-Banach Theorem for real vector spaces. So \<open>f\<close> can be
+    extended in a norm-preserving way to some function \<open>g\<close> on the whole
+    vector space \<open>E\<close>.\<close>
 
   with E FE linearform q obtain g where
       linearformE: "linearform E g"
@@ -445,19 +444,20 @@
   have "\<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
   proof (rule order_antisym)
     txt \<open>
-      First we show \<open>\<parallel>g\<parallel> \<le> \<parallel>f\<parallel>\<close>.  The function norm \<open>\<parallel>g\<parallel>\<close> is defined as the smallest \<open>c \<in> \<real>\<close> such that
+      First we show \<open>\<parallel>g\<parallel> \<le> \<parallel>f\<parallel>\<close>. The function norm \<open>\<parallel>g\<parallel>\<close> is defined as the
+      smallest \<open>c \<in> \<real>\<close> such that
       \begin{center}
       \begin{tabular}{l}
       \<open>\<forall>x \<in> E. \<bar>g x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
       \end{tabular}
       \end{center}
-      \noindent Furthermore holds
+      \<^noindent> Furthermore holds
       \begin{center}
       \begin{tabular}{l}
       \<open>\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>\<close>
       \end{tabular}
       \end{center}
-\<close>
+    \<close>
 
     from g_cont _ ge_zero
     show "\<parallel>g\<parallel>\<hyphen>E \<le> \<parallel>f\<parallel>\<hyphen>F"
diff -r a29295dac1ca -r f92bf6674699 src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Mon Nov 02 11:10:28 2015 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Mon Nov 02 11:43:02 2015 +0100
@@ -9,29 +9,27 @@
 begin
 
 text \<open>
-  In this section the following context is presumed.  Let \<open>E\<close> be
-  a real vector space with a seminorm \<open>q\<close> on \<open>E\<close>. \<open>F\<close> is a subspace of \<open>E\<close> and \<open>f\<close> a linear function on
-  \<open>F\<close>. We consider a subspace \<open>H\<close> of \<open>E\<close> that is a
-  superspace of \<open>F\<close> and a linear form \<open>h\<close> on \<open>H\<close>. \<open>H\<close> is a not equal to \<open>E\<close> and \<open>x\<^sub>0\<close> is
-  an element in \<open>E - H\<close>.  \<open>H\<close> is extended to the direct
-  sum \<open>H' = H + lin x\<^sub>0\<close>, so for any \<open>x \<in> H'\<close>
-  the decomposition of \<open>x = y + a \<cdot> x\<close> with \<open>y \<in> H\<close> is
-  unique. \<open>h'\<close> is defined on \<open>H'\<close> by \<open>h' x = h y +
-  a \<cdot> \<xi>\<close> for a certain \<open>\<xi>\<close>.
+  In this section the following context is presumed. Let \<open>E\<close> be a real
+  vector space with a seminorm \<open>q\<close> on \<open>E\<close>. \<open>F\<close> is a subspace of \<open>E\<close> and \<open>f\<close>
+  a linear function on \<open>F\<close>. We consider a subspace \<open>H\<close> of \<open>E\<close> that is a
+  superspace of \<open>F\<close> and a linear form \<open>h\<close> on \<open>H\<close>. \<open>H\<close> is a not equal to \<open>E\<close>
+  and \<open>x\<^sub>0\<close> is an element in \<open>E - H\<close>. \<open>H\<close> is extended to the direct sum \<open>H'
+  = H + lin x\<^sub>0\<close>, so for any \<open>x \<in> H'\<close> the decomposition of \<open>x = y + a \<cdot> x\<close>
+  with \<open>y \<in> H\<close> is unique. \<open>h'\<close> is defined on \<open>H'\<close> by \<open>h' x = h y + a \<cdot> \<xi>\<close>
+  for a certain \<open>\<xi>\<close>.
 
-  Subsequently we show some properties of this extension \<open>h'\<close> of
-  \<open>h\<close>.
+  Subsequently we show some properties of this extension \<open>h'\<close> of \<open>h\<close>.
 
   \<^medskip>
-  This lemma will be used to show the existence of a linear
-  extension of \<open>f\<close> (see page \pageref{ex-xi-use}). It is a
-  consequence of the completeness of \<open>\<real>\<close>. To show
+  This lemma will be used to show the existence of a linear extension of \<open>f\<close>
+  (see page \pageref{ex-xi-use}). It is a consequence of the completeness of
+  \<open>\<real>\<close>. To show
   \begin{center}
   \begin{tabular}{l}
   \<open>\<exists>\<xi>. \<forall>y \<in> F. a y \<le> \<xi> \<and> \<xi> \<le> b y\<close>
   \end{tabular}
   \end{center}
-  \noindent it suffices to show that
+  \<^noindent> it suffices to show that
   \begin{center}
   \begin{tabular}{l}
   \<open>\<forall>u \<in> F. \<forall>v \<in> F. a u \<le> b v\<close>
@@ -84,9 +82,8 @@
 
 text \<open>
   \<^medskip>
-  The function \<open>h'\<close> is defined as a \<open>h' x = h y
-  + a \<cdot> \<xi>\<close> where \<open>x = y + a \<cdot> \<xi>\<close> is a linear extension of
-  \<open>h\<close> to \<open>H'\<close>.
+  The function \<open>h'\<close> is defined as a \<open>h' x = h y + a \<cdot> \<xi>\<close> where
+  \<open>x = y + a \<cdot> \<xi>\<close> is a linear extension of \<open>h\<close> to \<open>H'\<close>.
 \<close>
 
 lemma h'_lf:
@@ -192,8 +189,8 @@
 
 text \<open>
   \<^medskip>
-  The linear extension \<open>h'\<close> of \<open>h\<close>
-  is bounded by the seminorm \<open>p\<close>.\<close>
+  The linear extension \<open>h'\<close> of \<open>h\<close> is bounded by the seminorm \<open>p\<close>.
+\<close>
 
 lemma h'_norm_pres:
   assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
diff -r a29295dac1ca -r f92bf6674699 src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Mon Nov 02 11:10:28 2015 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Mon Nov 02 11:43:02 2015 +0100
@@ -2,27 +2,25 @@
     Author:     Gertrud Bauer, TU Munich
 *)
 
-section \<open>The supremum w.r.t.~the function order\<close>
+section \<open>The supremum wrt.\ the function order\<close>
 
 theory Hahn_Banach_Sup_Lemmas
 imports Function_Norm Zorn_Lemma
 begin
 
 text \<open>
-  This section contains some lemmas that will be used in the proof of
-  the Hahn-Banach Theorem.  In this section the following context is
-  presumed.  Let \<open>E\<close> be a real vector space with a seminorm
-  \<open>p\<close> on \<open>E\<close>.  \<open>F\<close> is a subspace of \<open>E\<close> and
-  \<open>f\<close> a linear form on \<open>F\<close>. We consider a chain \<open>c\<close>
-  of norm-preserving extensions of \<open>f\<close>, such that \<open>\<Union>c =
-  graph H h\<close>.  We will show some properties about the limit function
-  \<open>h\<close>, i.e.\ the supremum of the chain \<open>c\<close>.
+  This section contains some lemmas that will be used in the proof of the
+  Hahn-Banach Theorem. In this section the following context is presumed.
+  Let \<open>E\<close> be a real vector space with a seminorm \<open>p\<close> on \<open>E\<close>. \<open>F\<close> is a
+  subspace of \<open>E\<close> and \<open>f\<close> a linear form on \<open>F\<close>. We consider a chain \<open>c\<close> of
+  norm-preserving extensions of \<open>f\<close>, such that \<open>\<Union>c = graph H h\<close>. We will
+  show some properties about the limit function \<open>h\<close>, i.e.\ the supremum of
+  the chain \<open>c\<close>.
 
   \<^medskip>
-  Let \<open>c\<close> be a chain of norm-preserving extensions of
-  the function \<open>f\<close> and let \<open>graph H h\<close> be the supremum
-  of \<open>c\<close>.  Every element in \<open>H\<close> is member of one of the
-  elements of the chain.
+  Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and
+  let \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in \<open>H\<close> is member of
+  one of the elements of the chain.
 \<close>
 
 lemmas [dest?] = chainsD
@@ -57,10 +55,10 @@
 
 text \<open>
   \<^medskip>
-  Let \<open>c\<close> be a chain of norm-preserving extensions of
-  the function \<open>f\<close> and let \<open>graph H h\<close> be the supremum
-  of \<open>c\<close>.  Every element in the domain \<open>H\<close> of the supremum
-  function is member of the domain \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close> extends \<open>h'\<close>.
+  Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and
+  let \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in the domain \<open>H\<close> of
+  the supremum function is member of the domain \<open>H'\<close> of some function \<open>h'\<close>,
+  such that \<open>h\<close> extends \<open>h'\<close>.
 \<close>
 
 lemma some_H'h':
@@ -85,10 +83,9 @@
 
 text \<open>
   \<^medskip>
-  Any two elements \<open>x\<close> and \<open>y\<close> in the domain
-  \<open>H\<close> of the supremum function \<open>h\<close> are both in the domain
-  \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close> extends
-  \<open>h'\<close>.
+  Any two elements \<open>x\<close> and \<open>y\<close> in the domain \<open>H\<close> of the supremum function
+  \<open>h\<close> are both in the domain \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close>
+  extends \<open>h'\<close>.
 \<close>
 
 lemma some_H'h'2:
@@ -158,8 +155,8 @@
 
 text \<open>
   \<^medskip>
-  The relation induced by the graph of the supremum of a
-  chain \<open>c\<close> is definite, i.~e.~t is the graph of a function.
+  The relation induced by the graph of the supremum of a chain \<open>c\<close> is
+  definite, i.e.\ it is the graph of a function.
 \<close>
 
 lemma sup_definite:
@@ -181,8 +178,8 @@
   then obtain H2 h2 where G2_rep: "G2 = graph H2 h2"
     unfolding M_def by blast
 
-  txt \<open>\<open>G\<^sub>1\<close> is contained in \<open>G\<^sub>2\<close>
-    or vice versa, since both \<open>G\<^sub>1\<close> and \<open>G\<^sub>2\<close> are members of \<open>c\<close>. \label{cases2}\<close>
+  txt \<open>\<open>G\<^sub>1\<close> is contained in \<open>G\<^sub>2\<close> or vice versa, since both \<open>G\<^sub>1\<close> and \<open>G\<^sub>2\<close>
+    are members of \<open>c\<close>. \label{cases2}\<close>
 
   from cM G1 G2 consider "G1 \<subseteq> G2" | "G2 \<subseteq> G1"
     by (blast dest: chainsD)
@@ -208,12 +205,11 @@
 
 text \<open>
   \<^medskip>
-  The limit function \<open>h\<close> is linear. Every element
-  \<open>x\<close> in the domain of \<open>h\<close> is in the domain of a function
-  \<open>h'\<close> in the chain of norm preserving extensions.  Furthermore,
-  \<open>h\<close> is an extension of \<open>h'\<close> so the function values of
-  \<open>x\<close> are identical for \<open>h'\<close> and \<open>h\<close>.  Finally, the
-  function \<open>h'\<close> is linear by construction of \<open>M\<close>.
+  The limit function \<open>h\<close> is linear. Every element \<open>x\<close> in the domain of \<open>h\<close>
+  is in the domain of a function \<open>h'\<close> in the chain of norm preserving
+  extensions. Furthermore, \<open>h\<close> is an extension of \<open>h'\<close> so the function
+  values of \<open>x\<close> are identical for \<open>h'\<close> and \<open>h\<close>. Finally, the function \<open>h'\<close>
+  is linear by construction of \<open>M\<close>.
 \<close>
 
 lemma sup_lf:
@@ -264,10 +260,9 @@
 
 text \<open>
   \<^medskip>
-  The limit of a non-empty chain of norm preserving
-  extensions of \<open>f\<close> is an extension of \<open>f\<close>, since every
-  element of the chain is an extension of \<open>f\<close> and the supremum
-  is an extension for every element of the chain.
+  The limit of a non-empty chain of norm preserving extensions of \<open>f\<close> is an
+  extension of \<open>f\<close>, since every element of the chain is an extension of \<open>f\<close>
+  and the supremum is an extension for every element of the chain.
 \<close>
 
 lemma sup_ext:
@@ -291,9 +286,8 @@
 
 text \<open>
   \<^medskip>
-  The domain \<open>H\<close> of the limit function is a superspace
-  of \<open>F\<close>, since \<open>F\<close> is a subset of \<open>H\<close>. The
-  existence of the \<open>0\<close> element in \<open>F\<close> and the closure
+  The domain \<open>H\<close> of the limit function is a superspace of \<open>F\<close>, since \<open>F\<close> is
+  a subset of \<open>H\<close>. The existence of the \<open>0\<close> element in \<open>F\<close> and the closure
   properties follow from the fact that \<open>F\<close> is a vector space.
 \<close>
 
@@ -317,8 +311,7 @@
 
 text \<open>
   \<^medskip>
-  The domain \<open>H\<close> of the limit function is a subspace of
-  \<open>E\<close>.
+  The domain \<open>H\<close> of the limit function is a subspace of \<open>E\<close>.
 \<close>
 
 lemma sup_subE:
@@ -374,8 +367,8 @@
 
 text \<open>
   \<^medskip>
-  The limit function is bounded by the norm \<open>p\<close> as
-  well, since all elements in the chain are bounded by \<open>p\<close>.
+  The limit function is bounded by the norm \<open>p\<close> as well, since all elements
+  in the chain are bounded by \<open>p\<close>.
 \<close>
 
 lemma sup_norm_pres:
@@ -396,10 +389,10 @@
 
 text \<open>
   \<^medskip>
-  The following lemma is a property of linear forms on real
-  vector spaces. It will be used for the lemma \<open>abs_Hahn_Banach\<close>
-  (see page \pageref{abs-Hahn_Banach}). \label{abs-ineq-iff} For real
-  vector spaces the following inequations are equivalent:
+  The following lemma is a property of linear forms on real vector spaces.
+  It will be used for the lemma \<open>abs_Hahn_Banach\<close> (see page
+  \pageref{abs-Hahn-Banach}). \label{abs-ineq-iff} For real vector spaces
+  the following inequality are equivalent:
   \begin{center}
   \begin{tabular}{lll}
   \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and &
diff -r a29295dac1ca -r f92bf6674699 src/HOL/Hahn_Banach/Linearform.thy
--- a/src/HOL/Hahn_Banach/Linearform.thy	Mon Nov 02 11:10:28 2015 +0100
+++ b/src/HOL/Hahn_Banach/Linearform.thy	Mon Nov 02 11:43:02 2015 +0100
@@ -9,8 +9,8 @@
 begin
 
 text \<open>
-  A \<^emph>\<open>linear form\<close> is a function on a vector space into the reals
-  that is additive and multiplicative.
+  A \<^emph>\<open>linear form\<close> is a function on a vector space into the reals that is
+  additive and multiplicative.
 \<close>
 
 locale linearform =
diff -r a29295dac1ca -r f92bf6674699 src/HOL/Hahn_Banach/Normed_Space.thy
--- a/src/HOL/Hahn_Banach/Normed_Space.thy	Mon Nov 02 11:10:28 2015 +0100
+++ b/src/HOL/Hahn_Banach/Normed_Space.thy	Mon Nov 02 11:43:02 2015 +0100
@@ -11,9 +11,9 @@
 subsection \<open>Quasinorms\<close>
 
 text \<open>
-  A \<^emph>\<open>seminorm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a function on a real vector space
-  into the reals that has the following properties: it is positive
-  definite, absolute homogeneous and subadditive.
+  A \<^emph>\<open>seminorm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a function on a real vector space into the reals
+  that has the following properties: it is positive definite, absolute
+  homogeneous and subadditive.
 \<close>
 
 locale seminorm =
diff -r a29295dac1ca -r f92bf6674699 src/HOL/Hahn_Banach/Subspace.thy
--- a/src/HOL/Hahn_Banach/Subspace.thy	Mon Nov 02 11:10:28 2015 +0100
+++ b/src/HOL/Hahn_Banach/Subspace.thy	Mon Nov 02 11:43:02 2015 +0100
@@ -11,9 +11,8 @@
 subsection \<open>Definition\<close>
 
 text \<open>
-  A non-empty subset \<open>U\<close> of a vector space \<open>V\<close> is a
-  \<^emph>\<open>subspace\<close> of \<open>V\<close>, iff \<open>U\<close> is closed under addition
-  and scalar multiplication.
+  A non-empty subset \<open>U\<close> of a vector space \<open>V\<close> is a \<^emph>\<open>subspace\<close> of \<open>V\<close>, iff
+  \<open>U\<close> is closed under addition and scalar multiplication.
 \<close>
 
 locale subspace =
@@ -51,9 +50,9 @@
 
 text \<open>
   \<^medskip>
-  Similar as for linear spaces, the existence of the zero
-  element in every subspace follows from the non-emptiness of the
-  carrier set and by vector space laws.
+  Similar as for linear spaces, the existence of the zero element in every
+  subspace follows from the non-emptiness of the carrier set and by vector
+  space laws.
 \<close>
 
 lemma (in subspace) zero [intro]:
@@ -140,8 +139,8 @@
 subsection \<open>Linear closure\<close>
 
 text \<open>
-  The \<^emph>\<open>linear closure\<close> of a vector \<open>x\<close> is the set of all
-  scalar multiples of \<open>x\<close>.
+  The \<^emph>\<open>linear closure\<close> of a vector \<open>x\<close> is the set of all scalar multiples
+  of \<open>x\<close>.
 \<close>
 
 definition lin :: "('a::{minus,plus,zero}) \<Rightarrow> 'a set"
@@ -227,8 +226,8 @@
 subsection \<open>Sum of two vectorspaces\<close>
 
 text \<open>
-  The \<^emph>\<open>sum\<close> of two vectorspaces \<open>U\<close> and \<open>V\<close> is the
-  set of all sums of elements from \<open>U\<close> and \<open>V\<close>.
+  The \<^emph>\<open>sum\<close> of two vectorspaces \<open>U\<close> and \<open>V\<close> is the set of all sums of
+  elements from \<open>U\<close> and \<open>V\<close>.
 \<close>
 
 lemma sum_def: "U + V = {u + v | u v. u \<in> U \<and> v \<in> V}"
@@ -329,10 +328,10 @@
 subsection \<open>Direct sums\<close>
 
 text \<open>
-  The sum of \<open>U\<close> and \<open>V\<close> is called \<^emph>\<open>direct\<close>, iff the
-  zero element is the only common element of \<open>U\<close> and \<open>V\<close>. For every element \<open>x\<close> of the direct sum of \<open>U\<close> and
-  \<open>V\<close> the decomposition in \<open>x = u + v\<close> with
-  \<open>u \<in> U\<close> and \<open>v \<in> V\<close> is unique.
+  The sum of \<open>U\<close> and \<open>V\<close> is called \<^emph>\<open>direct\<close>, iff the zero element is the
+  only common element of \<open>U\<close> and \<open>V\<close>. For every element \<open>x\<close> of the direct
+  sum of \<open>U\<close> and \<open>V\<close> the decomposition in \<open>x = u + v\<close> with \<open>u \<in> U\<close> and
+  \<open>v \<in> V\<close> is unique.
 \<close>
 
 lemma decomp:
@@ -377,12 +376,10 @@
 qed
 
 text \<open>
-  An application of the previous lemma will be used in the proof of
-  the Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any
-  element \<open>y + a \<cdot> x\<^sub>0\<close> of the direct sum of a
-  vectorspace \<open>H\<close> and the linear closure of \<open>x\<^sub>0\<close>
-  the components \<open>y \<in> H\<close> and \<open>a\<close> are uniquely
-  determined.
+  An application of the previous lemma will be used in the proof of the
+  Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any element
+  \<open>y + a \<cdot> x\<^sub>0\<close> of the direct sum of a vectorspace \<open>H\<close> and the linear closure
+  of \<open>x\<^sub>0\<close> the components \<open>y \<in> H\<close> and \<open>a\<close> are uniquely determined.
 \<close>
 
 lemma decomp_H':
@@ -436,10 +433,9 @@
 qed
 
 text \<open>
-  Since for any element \<open>y + a \<cdot> x'\<close> of the direct sum of a
-  vectorspace \<open>H\<close> and the linear closure of \<open>x'\<close> the
-  components \<open>y \<in> H\<close> and \<open>a\<close> are unique, it follows from
-  \<open>y \<in> H\<close> that \<open>a = 0\<close>.
+  Since for any element \<open>y + a \<cdot> x'\<close> of the direct sum of a vectorspace \<open>H\<close>
+  and the linear closure of \<open>x'\<close> the components \<open>y \<in> H\<close> and \<open>a\<close> are unique,
+  it follows from \<open>y \<in> H\<close> that \<open>a = 0\<close>.
 \<close>
 
 lemma decomp_H'_H:
@@ -464,9 +460,8 @@
 qed
 
 text \<open>
-  The components \<open>y \<in> H\<close> and \<open>a\<close> in \<open>y + a \<cdot> x'\<close>
-  are unique, so the function \<open>h'\<close> defined by
-  \<open>h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>\<close> is definite.
+  The components \<open>y \<in> H\<close> and \<open>a\<close> in \<open>y + a \<cdot> x'\<close> are unique, so the function
+  \<open>h'\<close> defined by \<open>h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>\<close> is definite.
 \<close>
 
 lemma h'_definite:
diff -r a29295dac1ca -r f92bf6674699 src/HOL/Hahn_Banach/Vector_Space.thy
--- a/src/HOL/Hahn_Banach/Vector_Space.thy	Mon Nov 02 11:10:28 2015 +0100
+++ b/src/HOL/Hahn_Banach/Vector_Space.thy	Mon Nov 02 11:43:02 2015 +0100
@@ -11,9 +11,9 @@
 subsection \<open>Signature\<close>
 
 text \<open>
-  For the definition of real vector spaces a type @{typ 'a} of the
-  sort \<open>{plus, minus, zero}\<close> is considered, on which a real
-  scalar multiplication \<open>\<cdot>\<close> is declared.
+  For the definition of real vector spaces a type @{typ 'a} of the sort
+  \<open>{plus, minus, zero}\<close> is considered, on which a real scalar multiplication
+  \<open>\<cdot>\<close> is declared.
 \<close>
 
 consts
@@ -23,13 +23,13 @@
 subsection \<open>Vector space laws\<close>
 
 text \<open>
-  A \<^emph>\<open>vector space\<close> is a non-empty set \<open>V\<close> of elements from
-  @{typ 'a} with the following vector space laws: The set \<open>V\<close> is
-  closed under addition and scalar multiplication, addition is
-  associative and commutative; \<open>- x\<close> is the inverse of \<open>x\<close> w.~r.~t.~addition and \<open>0\<close> is the neutral element of
-  addition.  Addition and multiplication are distributive; scalar
-  multiplication is associative and the real number \<open>1\<close> is
-  the neutral element of scalar multiplication.
+  A \<^emph>\<open>vector space\<close> is a non-empty set \<open>V\<close> of elements from @{typ 'a} with
+  the following vector space laws: The set \<open>V\<close> is closed under addition and
+  scalar multiplication, addition is associative and commutative; \<open>- x\<close> is
+  the inverse of \<open>x\<close> wrt.\ addition and \<open>0\<close> is the neutral element of
+  addition. Addition and multiplication are distributive; scalar
+  multiplication is associative and the real number \<open>1\<close> is the neutral
+  element of scalar multiplication.
 \<close>
 
 locale vectorspace =
@@ -64,7 +64,8 @@
 lemma neg_closed [iff]: "x \<in> V \<Longrightarrow> - x \<in> V"
   by (simp add: negate_eq1)
 
-lemma add_left_commute: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)"
+lemma add_left_commute:
+  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)"
 proof -
   assume xyz: "x \<in> V"  "y \<in> V"  "z \<in> V"
   then have "x + (y + z) = (x + y) + z"
@@ -77,8 +78,8 @@
 lemmas add_ac = add_assoc add_commute add_left_commute
 
 
-text \<open>The existence of the zero element of a vector space
-  follows from the non-emptiness of carrier set.\<close>
+text \<open>The existence of the zero element of a vector space follows from the
+  non-emptiness of carrier set.\<close>
 
 lemma zero [iff]: "0 \<in> V"
 proof -
@@ -213,7 +214,8 @@
   then show "x + y = x + z" by (simp only:)
 qed
 
-lemma add_right_cancel: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (y + x = z + x) = (y = z)"
+lemma add_right_cancel:
+    "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (y + x = z + x) = (y = z)"
   by (simp only: add_commute add_left_cancel)
 
 lemma add_assoc_cong:
@@ -371,4 +373,3 @@
 end
 
 end
-
diff -r a29295dac1ca -r f92bf6674699 src/HOL/Hahn_Banach/document/root.tex
--- a/src/HOL/Hahn_Banach/document/root.tex	Mon Nov 02 11:10:28 2015 +0100
+++ b/src/HOL/Hahn_Banach/document/root.tex	Mon Nov 02 11:43:02 2015 +0100
@@ -16,7 +16,7 @@
 \pagenumbering{arabic}
 
 \title{The Hahn-Banach Theorem \\ for Real Vector Spaces}
-\author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}}
+\author{Gertrud Bauer}
 \maketitle
 
 \begin{abstract}