# HG changeset patch
# User wenzelm
# Date 1450616162 -3600
# Node ID e4f9d8f094fe9248147481d063cc07dc04e5905a
# Parent  fa4dbb82732fc28f869bd0889702e83e39ee033e
tuned whitespace;

diff -r fa4dbb82732f -r e4f9d8f094fe src/HOL/Hahn_Banach/Function_Norm.thy
--- a/src/HOL/Hahn_Banach/Function_Norm.thy	Sun Dec 20 13:11:47 2015 +0100
+++ b/src/HOL/Hahn_Banach/Function_Norm.thy	Sun Dec 20 13:56:02 2015 +0100
@@ -11,8 +11,8 @@
 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}
@@ -52,20 +52,20 @@
   \<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:
   \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 =
diff -r fa4dbb82732f -r e4f9d8f094fe src/HOL/Hahn_Banach/Function_Order.thy
--- a/src/HOL/Hahn_Banach/Function_Order.thy	Sun Dec 20 13:11:47 2015 +0100
+++ b/src/HOL/Hahn_Banach/Function_Order.thy	Sun Dec 20 13:56:02 2015 +0100
@@ -11,14 +11,12 @@
 subsection \<open>The graph of a function\<close>
 
 text \<open>
-  We define the \<^emph>\<open>graph\<close> of a (real) function \<open>f\<close> with
-  domain \<open>F\<close> as the set
+  We define the \<^emph>\<open>graph\<close> of a (real) function \<open>f\<close> with domain \<open>F\<close> as the set
   \begin{center}
   \<open>{(x, f x). x \<in> F}\<close>
   \end{center}
-  So we are modeling partial functions by specifying the domain and
-  the mapping function. We use the term ``function'' also for its
-  graph.
+  So we are modeling partial functions by specifying the domain and the
+  mapping function. We use the term ``function'' also for its graph.
 \<close>
 
 type_synonym 'a graph = "('a \<times> real) set"
@@ -41,8 +39,8 @@
 subsection \<open>Functions ordered by domain extension\<close>
 
 text \<open>
-  A function \<open>h'\<close> is an extension of \<open>h\<close>, iff the graph of
-  \<open>h\<close> is a subset of the graph of \<open>h'\<close>.
+  A function \<open>h'\<close> is an extension of \<open>h\<close>, iff the graph of \<open>h\<close> is a subset of
+  the graph of \<open>h'\<close>.
 \<close>
 
 lemma graph_extI:
@@ -93,8 +91,8 @@
 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
+  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>
 
diff -r fa4dbb82732f -r e4f9d8f094fe src/HOL/Hahn_Banach/Hahn_Banach.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Sun Dec 20 13:11:47 2015 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Sun Dec 20 13:56:02 2015 +0100
@@ -18,28 +18,26 @@
 
 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>.
+  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> 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:
 
-    \<^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>
@@ -292,14 +290,13 @@
 
 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 inequality 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 &
-  \<open>\<forall>x \<in> H. h x \<le> p x\<close> \\
+  \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and & \<open>\<forall>x \<in> H. h x \<le> p x\<close> \\
   \end{tabular}
   \end{center}
 \<close>
@@ -336,9 +333,8 @@
 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 +416,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"
diff -r fa4dbb82732f -r e4f9d8f094fe src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Sun Dec 20 13:11:47 2015 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Sun Dec 20 13:56:02 2015 +0100
@@ -9,14 +9,13 @@
 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>.
 
@@ -82,8 +81,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:
diff -r fa4dbb82732f -r e4f9d8f094fe src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Sun Dec 20 13:11:47 2015 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Sun Dec 20 13:56:02 2015 +0100
@@ -10,17 +10,16 @@
 
 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>.
+  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
@@ -55,10 +54,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':
@@ -83,9 +82,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:
@@ -99,8 +98,8 @@
     \<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H'
     \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
 proof -
-  txt \<open>\<open>y\<close> is in the domain \<open>H''\<close> of some function \<open>h''\<close>,
-  such that \<open>h\<close> extends \<open>h''\<close>.\<close>
+  txt \<open>\<open>y\<close> is in the domain \<open>H''\<close> of some function \<open>h''\<close>, such that \<open>h\<close>
+    extends \<open>h''\<close>.\<close>
 
   from M cM u and y obtain H' h' where
       y_hy: "(y, h y) \<in> graph H' h'"
@@ -121,10 +120,9 @@
       "graph F f \<subseteq> graph H'' h''"  "\<forall>x \<in> H''. h'' x \<le> p x"
     by (rule some_H'h't [elim_format]) blast
 
-  txt \<open>Since both \<open>h'\<close> and \<open>h''\<close> are elements of the chain,
-    \<open>h''\<close> is an extension of \<open>h'\<close> or vice versa. Thus both
-    \<open>x\<close> and \<open>y\<close> are contained in the greater
-    one. \label{cases1}\<close>
+  txt \<open>Since both \<open>h'\<close> and \<open>h''\<close> are elements of the chain, \<open>h''\<close> is an
+    extension of \<open>h'\<close> or vice versa. Thus both \<open>x\<close> and \<open>y\<close> are contained in
+    the greater one. \label{cases1}\<close>
 
   from cM c'' c' consider "graph H'' h'' \<subseteq> graph H' h'" | "graph H' h' \<subseteq> graph H'' h''"
     by (blast dest: chainsD)
@@ -205,11 +203,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:
@@ -286,8 +284,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>
 
@@ -367,8 +365,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:
@@ -389,10 +387,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 inequality 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 fa4dbb82732f -r e4f9d8f094fe src/HOL/Hahn_Banach/Normed_Space.thy
--- a/src/HOL/Hahn_Banach/Normed_Space.thy	Sun Dec 20 13:11:47 2015 +0100
+++ b/src/HOL/Hahn_Banach/Normed_Space.thy	Sun Dec 20 13:56: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 =
@@ -57,8 +57,7 @@
 subsection \<open>Norms\<close>
 
 text \<open>
-  A \<^emph>\<open>norm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a seminorm that maps only the
-  \<open>0\<close> vector to \<open>0\<close>.
+  A \<^emph>\<open>norm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a seminorm that maps only the \<open>0\<close> vector to \<open>0\<close>.
 \<close>
 
 locale norm = seminorm +
@@ -68,8 +67,7 @@
 subsection \<open>Normed vector spaces\<close>
 
 text \<open>
-  A vector space together with a norm is called a \<^emph>\<open>normed
-  space\<close>.
+  A vector space together with a norm is called a \<^emph>\<open>normed space\<close>.
 \<close>
 
 locale normed_vectorspace = vectorspace + norm
diff -r fa4dbb82732f -r e4f9d8f094fe src/HOL/Hahn_Banach/Subspace.thy
--- a/src/HOL/Hahn_Banach/Subspace.thy	Sun Dec 20 13:11:47 2015 +0100
+++ b/src/HOL/Hahn_Banach/Subspace.thy	Sun Dec 20 13:56:02 2015 +0100
@@ -139,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"
@@ -318,7 +318,7 @@
   qed
 qed
 
-text\<open>The sum of two subspaces is a vectorspace.\<close>
+text \<open>The sum of two subspaces is a vectorspace.\<close>
 
 lemma sum_vs [intro?]:
     "U \<unlhd> E \<Longrightarrow> V \<unlhd> E \<Longrightarrow> vectorspace E \<Longrightarrow> vectorspace (U + V)"
@@ -328,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:
@@ -434,8 +434,8 @@
 
 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>.
+  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:
diff -r fa4dbb82732f -r e4f9d8f094fe src/HOL/Hahn_Banach/Vector_Space.thy
--- a/src/HOL/Hahn_Banach/Vector_Space.thy	Sun Dec 20 13:11:47 2015 +0100
+++ b/src/HOL/Hahn_Banach/Vector_Space.thy	Sun Dec 20 13:56:02 2015 +0100
@@ -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> 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.
+  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 =
@@ -78,8 +78,10 @@
 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 -
diff -r fa4dbb82732f -r e4f9d8f094fe src/HOL/Hahn_Banach/Zorn_Lemma.thy
--- a/src/HOL/Hahn_Banach/Zorn_Lemma.thy	Sun Dec 20 13:11:47 2015 +0100
+++ b/src/HOL/Hahn_Banach/Zorn_Lemma.thy	Sun Dec 20 13:56:02 2015 +0100
@@ -9,13 +9,13 @@
 begin
 
 text \<open>
-  Zorn's Lemmas states: if every linear ordered subset of an ordered
-  set \<open>S\<close> has an upper bound in \<open>S\<close>, then there exists a
-  maximal element in \<open>S\<close>.  In our application, \<open>S\<close> is a
-  set of sets ordered by set inclusion. Since the union of a chain of
-  sets is an upper bound for all elements of the chain, the conditions
-  of Zorn's lemma can be modified: if \<open>S\<close> is non-empty, it
-  suffices to show that for every non-empty chain \<open>c\<close> in \<open>S\<close> the union of \<open>c\<close> also lies in \<open>S\<close>.
+  Zorn's Lemmas states: if every linear ordered subset of an ordered set \<open>S\<close>
+  has an upper bound in \<open>S\<close>, then there exists a maximal element in \<open>S\<close>. In
+  our application, \<open>S\<close> is a set of sets ordered by set inclusion. Since the
+  union of a chain of sets is an upper bound for all elements of the chain,
+  the conditions of Zorn's lemma can be modified: if \<open>S\<close> is non-empty, it
+  suffices to show that for every non-empty chain \<open>c\<close> in \<open>S\<close> the union of \<open>c\<close>
+  also lies in \<open>S\<close>.
 \<close>
 
 theorem Zorn's_Lemma:
@@ -28,16 +28,14 @@
     fix c assume "c \<in> chains S"
     show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"
     proof cases
-
-      txt \<open>If \<open>c\<close> is an empty chain, then every element in
-        \<open>S\<close> is an upper bound of \<open>c\<close>.\<close>
+      txt \<open>If \<open>c\<close> is an empty chain, then every element in \<open>S\<close> is an upper
+        bound of \<open>c\<close>.\<close>
 
       assume "c = {}"
       with aS show ?thesis by fast
 
-      txt \<open>If \<open>c\<close> is non-empty, then \<open>\<Union>c\<close> is an upper
-        bound of \<open>c\<close>, lying in \<open>S\<close>.\<close>
-
+      txt \<open>If \<open>c\<close> is non-empty, then \<open>\<Union>c\<close> is an upper bound of \<open>c\<close>, lying in
+        \<open>S\<close>.\<close>
     next
       assume "c \<noteq> {}"
       show ?thesis