# HG changeset patch
# User wenzelm
# Date 1446459028 -3600
# Node ID a29295dac1ca8425b072bfd03bef59405d0d39c9
# Parent  bf4969660913658153c4e17e530a2f69c02683c4
isabelle update_cartouches -t;

diff -r bf4969660913 -r a29295dac1ca src/HOL/Hahn_Banach/Function_Norm.thy
--- a/src/HOL/Hahn_Banach/Function_Norm.thy	Mon Nov 02 10:38:42 2015 +0100
+++ b/src/HOL/Hahn_Banach/Function_Norm.thy	Mon Nov 02 11:10:28 2015 +0100
@@ -11,10 +11,10 @@
 subsection \<open>Continuous linear forms\<close>
 
 text \<open>
-  A linear form @{text f} on a normed vector space @{text "(V, \<parallel>\<cdot>\<parallel>)"}
+  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}
-  @{text "\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+  \<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
@@ -42,33 +42,33 @@
 subsection \<open>The norm of a linear form\<close>
 
 text \<open>
-  The least real number @{text c} for which holds
+  The least real number \<open>c\<close> for which holds
   \begin{center}
-  @{text "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+  \<open>\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
   \end{center}
-  is called the \<^emph>\<open>norm\<close> of @{text f}.
+  is called the \<^emph>\<open>norm\<close> of \<open>f\<close>.
 
-  For non-trivial vector spaces @{text "V \<noteq> {0}"} the norm can be
+  For non-trivial vector spaces \<open>V \<noteq> {0}\<close> the norm can be
   defined as
   \begin{center}
-  @{text "\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>"}
+  \<open>\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>\<close>
   \end{center}
 
-  For the case @{text "V = {0}"} the supremum would be taken from an
-  empty set. Since @{text \<real>} is unbounded, there would be no supremum.
+  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 @{text "{} \<ge> 0"} so that
-  @{text fn_norm} has the norm properties. Furthermore it does not
-  have to change the norm in all other cases, so it must be @{text 0},
-  as all other elements are @{text "{} \<ge> 0"}.
+  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 @{text B} where the supremum is taken from as
+  Thus we define the set \<open>B\<close> where the supremum is taken from as
   follows:
   \begin{center}
-  @{text "{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}"}
+  \<open>{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}\<close>
   \end{center}
 
-  @{text fn_norm} is equal to the supremum of @{text B}, if the
+  \<open>fn_norm\<close> is equal to the supremum of \<open>B\<close>, if the
   supremum exists (otherwise it is undefined).
 \<close>
 
@@ -85,7 +85,7 @@
 
 text \<open>
   The following lemma states that every continuous linear form on a
-  normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm.
+  normed space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> has a function norm.
 \<close>
 
 lemma (in normed_vectorspace_with_fn_norm) fn_norm_works:
@@ -98,19 +98,19 @@
     non-empty bounded set of reals has a supremum.\<close>
   have "\<exists>a. lub (B V f) a"
   proof (rule real_complete)
-    txt \<open>First we have to show that @{text B} is non-empty:\<close>
+    txt \<open>First we have to show that \<open>B\<close> is non-empty:\<close>
     have "0 \<in> B V f" ..
     then show "\<exists>x. x \<in> B V f" ..
 
-    txt \<open>Then we have to show that @{text B} is bounded:\<close>
+    txt \<open>Then we have to show that \<open>B\<close> is bounded:\<close>
     show "\<exists>c. \<forall>y \<in> B V f. y \<le> c"
     proof -
-      txt \<open>We know that @{text f} is bounded by some value @{text c}.\<close>
+      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
-        @{text b}, such that @{text "y \<le> b"} for all @{text "y \<in>
-        B"}. Due to the definition of @{text B} there are two cases.\<close>
+        \<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"
@@ -121,8 +121,8 @@
           assume "y = 0"
           then show ?thesis unfolding b_def by arith
         next
-          txt \<open>The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
-            @{text "x \<in> V"} with @{text "x \<noteq> 0"}.\<close>
+          txt \<open>The second case is \<open>y = \<bar>f x\<bar> / \<parallel>x\<parallel>\<close> for some
+            \<open>x \<in> V\<close> with \<open>x \<noteq> 0\<close>.\<close>
           assume "y \<noteq> 0"
           with y obtain x where y_rep: "y = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
               and x: "x \<in> V" and neq: "x \<noteq> 0"
@@ -130,7 +130,7 @@
           from x neq have gt: "0 < \<parallel>x\<parallel>" ..
 
           txt \<open>The thesis follows by a short calculation using the
-            fact that @{text f} is bounded.\<close>
+            fact that \<open>f\<close> is bounded.\<close>
 
           note y_rep
           also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
@@ -177,16 +177,16 @@
   from this and b show ?thesis ..
 qed
 
-text \<open>The norm of a continuous function is always @{text "\<ge> 0"}.\<close>
+text \<open>The norm of a continuous function is always \<open>\<ge> 0\<close>.\<close>
 
 lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]:
   assumes "continuous V f norm"
   shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
 proof -
   interpret continuous V f norm by fact
-  txt \<open>The function norm is defined as the supremum of @{text B}.
-    So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge>
-    0"}, provided the supremum exists and @{text B} is not empty.\<close>
+  txt \<open>The function norm is defined as the supremum of \<open>B\<close>.
+    So it is \<open>\<ge> 0\<close> if all elements in \<open>B\<close> are \<open>\<ge>
+    0\<close>, provided the supremum exists and \<open>B\<close> is not empty.\<close>
   have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
     using \<open>continuous V f norm\<close> by (rule fn_norm_works)
   moreover have "0 \<in> B V f" ..
@@ -197,7 +197,7 @@
   \<^medskip>
   The fundamental property of function norms is:
   \begin{center}
-  @{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
+  \<open>\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>\<close>
   \end{center}
 \<close>
 
@@ -240,7 +240,7 @@
   The function norm is the least positive real number for
   which the following inequation holds:
   \begin{center}
-    @{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+    \<open>\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
   \end{center}
 \<close>
 
diff -r bf4969660913 -r a29295dac1ca src/HOL/Hahn_Banach/Function_Order.thy
--- a/src/HOL/Hahn_Banach/Function_Order.thy	Mon Nov 02 10:38:42 2015 +0100
+++ b/src/HOL/Hahn_Banach/Function_Order.thy	Mon Nov 02 11:10:28 2015 +0100
@@ -11,10 +11,10 @@
 subsection \<open>The graph of a function\<close>
 
 text \<open>
-  We define the \<^emph>\<open>graph\<close> of a (real) function @{text f} with
-  domain @{text F} 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}
-  @{text "{(x, f x). x \<in> F}"}
+  \<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
@@ -41,8 +41,8 @@
 subsection \<open>Functions ordered by domain extension\<close>
 
 text \<open>
-  A function @{text h'} is an extension of @{text h}, iff the graph of
-  @{text h} is a subset of the graph of @{text h'}.
+  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:
@@ -60,8 +60,7 @@
 subsection \<open>Domain and function of a graph\<close>
 
 text \<open>
-  The inverse functions to @{text graph} are @{text domain} and @{text
-  funct}.
+  The inverse functions to \<open>graph\<close> are \<open>domain\<close> and \<open>funct\<close>.
 \<close>
 
 definition domain :: "'a graph \<Rightarrow> 'a set"
@@ -71,8 +70,8 @@
   where "funct g = (\<lambda>x. (SOME y. (x, y) \<in> g))"
 
 text \<open>
-  The following lemma states that @{text g} is the graph of a function
-  if the relation induced by @{text g} 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:
@@ -94,10 +93,9 @@
 subsection \<open>Norm-preserving extensions of a function\<close>
 
 text \<open>
-  Given a linear form @{text f} on the space @{text F} and a seminorm
-  @{text p} on @{text E}. The set of all linear extensions of @{text
-  f}, to superspaces @{text H} of @{text F}, which are bounded by
-  @{text p}, 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 bf4969660913 -r a29295dac1ca src/HOL/Hahn_Banach/Hahn_Banach.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Mon Nov 02 10:38:42 2015 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Mon Nov 02 11:10:28 2015 +0100
@@ -17,34 +17,31 @@
 
 paragraph \<open>Hahn-Banach Theorem.\<close>
 text \<open>
-  Let @{text F} be a subspace of a real vector space @{text E}, let @{text
-  p} be a semi-norm on @{text E}, and @{text f} be a linear form defined on
-  @{text F} such that @{text f} is bounded by @{text p}, i.e. @{text "\<forall>x \<in>
-  F. f x \<le> p x"}. Then @{text f} can be extended to a linear form @{text h}
-  on @{text E} such that @{text h} is norm-preserving, i.e. @{text h} is
-  also bounded by @{text p}.
+  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 @{text M} as the set of norm-preserving extensions of
-  @{text f} to subspaces of @{text E}. The linear forms in @{text M}
+  \<^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 @{text M} has an upper
-  bound in @{text M}.
+  \<^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
-  @{text g} in @{text M}.
+  \<open>g\<close> in \<open>M\<close>.
 
-  \<^enum> The domain @{text H} of @{text g} is the whole space @{text
-  E}, 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 @{text g} is not defined on whole @{text E}, it can
-    still be extended in a norm-preserving way to a super-space @{text
-    H'} of @{text H}.
+    \<^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 @{text g} can not be maximal. Contradiction!
+    \<^item> Thus \<open>g\<close> can not be maximal. Contradiction!
 \<close>
 
 theorem Hahn_Banach:
@@ -52,9 +49,9 @@
     and "seminorm E p" and "linearform F f"
   assumes fp: "\<forall>x \<in> F. f x \<le> p x"
   shows "\<exists>h. linearform E h \<and> (\<forall>x \<in> F. h x = f x) \<and> (\<forall>x \<in> E. h x \<le> p x)"
-    -- \<open>Let @{text E} be a vector space, @{text F} a subspace of @{text E}, @{text p} a seminorm on @{text E},\<close>
-    -- \<open>and @{text f} a linear form on @{text F} such that @{text f} is bounded by @{text p},\<close>
-    -- \<open>then @{text f} can be extended to a linear form @{text h} on @{text E} in a norm-preserving way. \<^smallskip>\<close>
+    -- \<open>Let \<open>E\<close> be a vector space, \<open>F\<close> a subspace of \<open>E\<close>, \<open>p\<close> a seminorm on \<open>E\<close>,\<close>
+    -- \<open>and \<open>f\<close> a linear form on \<open>F\<close> such that \<open>f\<close> is bounded by \<open>p\<close>,\<close>
+    -- \<open>then \<open>f\<close> can be extended to a linear form \<open>h\<close> on \<open>E\<close> in a norm-preserving way. \<^smallskip>\<close>
 proof -
   interpret vectorspace E by fact
   interpret subspace F E by fact
@@ -67,8 +64,8 @@
   {
     fix c assume cM: "c \<in> chains M" and ex: "\<exists>x. x \<in> c"
     have "\<Union>c \<in> M"
-      -- \<open>Show that every non-empty chain @{text c} of @{text M} has an upper bound in @{text M}:\<close>
-      -- \<open>@{text "\<Union>c"} is greater than any element of the chain @{text c}, so it suffices to show @{text "\<Union>c \<in> M"}.\<close>
+      -- \<open>Show that every non-empty chain \<open>c\<close> of \<open>M\<close> has an upper bound in \<open>M\<close>:\<close>
+      -- \<open>\<open>\<Union>c\<close> is greater than any element of the chain \<open>c\<close>, so it suffices to show \<open>\<Union>c \<in> M\<close>.\<close>
       unfolding M_def
     proof (rule norm_pres_extensionI)
       let ?H = "domain (\<Union>c)"
@@ -98,9 +95,9 @@
     qed
   }
   then have "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x \<longrightarrow> x = g"
-  -- \<open>With Zorn's Lemma we can conclude that there is a maximal element in @{text M}. \<^smallskip>\<close>
+  -- \<open>With Zorn's Lemma we can conclude that there is a maximal element in \<open>M\<close>. \<^smallskip>\<close>
   proof (rule Zorn's_Lemma)
-      -- \<open>We show that @{text M} is non-empty:\<close>
+      -- \<open>We show that \<open>M\<close> is non-empty:\<close>
     show "graph F f \<in> M"
       unfolding M_def
     proof (rule norm_pres_extensionI2)
@@ -119,18 +116,18 @@
     and HE: "H \<unlhd> E" and FH: "F \<unlhd> H"
     and graphs: "graph F f \<subseteq> graph H h"
     and hp: "\<forall>x \<in> H. h x \<le> p x" unfolding M_def ..
-      -- \<open>@{text g} is a norm-preserving extension of @{text f}, in other words:\<close>
-      -- \<open>@{text g} is the graph of some linear form @{text h} defined on a subspace @{text H} of @{text E},\<close>
-      -- \<open>and @{text h} is an extension of @{text f} that is again bounded by @{text p}. \<^smallskip>\<close>
+      -- \<open>\<open>g\<close> is a norm-preserving extension of \<open>f\<close>, in other words:\<close>
+      -- \<open>\<open>g\<close> is the graph of some linear form \<open>h\<close> defined on a subspace \<open>H\<close> of \<open>E\<close>,\<close>
+      -- \<open>and \<open>h\<close> is an extension of \<open>f\<close> that is again bounded by \<open>p\<close>. \<^smallskip>\<close>
   from HE E have H: "vectorspace H"
     by (rule subspace.vectorspace)
 
   have HE_eq: "H = E"
-    -- \<open>We show that @{text h} is defined on whole @{text E} by classical contradiction. \<^smallskip>\<close>
+    -- \<open>We show that \<open>h\<close> is defined on whole \<open>E\<close> by classical contradiction. \<^smallskip>\<close>
   proof (rule classical)
     assume neq: "H \<noteq> E"
-      -- \<open>Assume @{text h} is not defined on whole @{text E}. Then show that @{text h} can be extended\<close>
-      -- \<open>in a norm-preserving way to a function @{text h'} with the graph @{text g'}. \<^smallskip>\<close>
+      -- \<open>Assume \<open>h\<close> is not defined on whole \<open>E\<close>. Then show that \<open>h\<close> can be extended\<close>
+      -- \<open>in a norm-preserving way to a function \<open>h'\<close> with the graph \<open>g'\<close>. \<^smallskip>\<close>
     have "\<exists>g' \<in> M. g \<subseteq> g' \<and> g \<noteq> g'"
     proof -
       from HE have "H \<subseteq> E" ..
@@ -146,7 +143,7 @@
       qed
 
       def H' \<equiv> "H + lin x'"
-        -- \<open>Define @{text H'} as the direct sum of @{text H} and the linear closure of @{text x'}. \<^smallskip>\<close>
+        -- \<open>Define \<open>H'\<close> as the direct sum of \<open>H\<close> and the linear closure of \<open>x'\<close>. \<^smallskip>\<close>
       have HH': "H \<unlhd> H'"
       proof (unfold H'_def)
         from x'E have "vectorspace (lin x')" ..
@@ -156,8 +153,8 @@
       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 @{text \<xi>} that fulfills certain inequations; this will\<close>
-        -- \<open>be used to establish that @{text h'} is a norm-preserving extension of @{text h}.
+        -- \<open>Pick a real number \<open>\<xi>\<close> that fulfills certain inequations; 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 -
         from H have "\<exists>xi. \<forall>y \<in> H. - p (y + x') - h y \<le> xi
@@ -185,10 +182,10 @@
 
       def h' \<equiv> "\<lambda>x. let (y, a) =
           SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H in h y + a * xi"
-        -- \<open>Define the extension @{text h'} of @{text h} to @{text H'} using @{text \<xi>}. \<^smallskip>\<close>
+        -- \<open>Define the extension \<open>h'\<close> of \<open>h\<close> to \<open>H'\<close> using \<open>\<xi>\<close>. \<^smallskip>\<close>
 
       have "g \<subseteq> graph H' h' \<and> g \<noteq> graph H' h'"
-        -- \<open>@{text h'} is an extension of @{text h} \dots \<^smallskip>\<close>
+        -- \<open>\<open>h'\<close> is an extension of \<open>h\<close> \dots \<^smallskip>\<close>
       proof
         show "g \<subseteq> graph H' h'"
         proof -
@@ -225,7 +222,7 @@
         qed
       qed
       moreover have "graph H' h' \<in> M"
-        -- \<open>and @{text h'} is norm-preserving. \<^smallskip>\<close>
+        -- \<open>and \<open>h'\<close> is norm-preserving. \<^smallskip>\<close>
       proof (unfold M_def)
         show "graph H' h' \<in> norm_pres_extensions E p F f"
         proof (rule norm_pres_extensionI2)
@@ -273,7 +270,7 @@
       ultimately show ?thesis ..
     qed
     then have "\<not> (\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x)" by simp
-      -- \<open>So the graph @{text g} of @{text h} cannot be maximal. Contradiction! \<^smallskip>\<close>
+      -- \<open>So the graph \<open>g\<close> of \<open>h\<close> cannot be maximal. Contradiction! \<^smallskip>\<close>
     with gx show "H = E" by contradiction
   qed
 
@@ -296,13 +293,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 @{text f} and a seminorm @{text p} the following inequations
+  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}).}
   \begin{center}
   \begin{tabular}{lll}
-  @{text "\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x"} & and &
-  @{text "\<forall>x \<in> H. h x \<le> p x"} \\
+  \<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>
@@ -339,9 +336,9 @@
 subsection \<open>The Hahn-Banach Theorem for normed spaces\<close>
 
 text \<open>
-  Every continuous linear form @{text f} on a subspace @{text F} of a
-  norm space @{text E}, can be extended to a continuous linear form
-  @{text g} on @{text E} such that @{text "\<parallel>f\<parallel> = \<parallel>g\<parallel>"}.
+  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:
@@ -370,22 +367,22 @@
     by (rule normed_vectorspace_with_fn_norm.fn_norm_ge_zero
       [OF normed_vectorspace_with_fn_norm.intro,
        OF F_norm \<open>continuous F f norm\<close> , folded B_def fn_norm_def])
-  txt \<open>We define a function @{text p} on @{text E} as follows:
-    @{text "p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}\<close>
+  txt \<open>We define a function \<open>p\<close> on \<open>E\<close> as follows:
+    \<open>p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>\<close>\<close>
   def p \<equiv> "\<lambda>x. \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
 
-  txt \<open>@{text p} is a seminorm on @{text E}:\<close>
+  txt \<open>\<open>p\<close> is a seminorm on \<open>E\<close>:\<close>
   have q: "seminorm E p"
   proof
     fix x y a assume x: "x \<in> E" and y: "y \<in> E"
     
-    txt \<open>@{text p} is positive definite:\<close>
+    txt \<open>\<open>p\<close> is positive definite:\<close>
     have "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero)
     moreover from x have "0 \<le> \<parallel>x\<parallel>" ..
     ultimately show "0 \<le> p x"  
       by (simp add: p_def zero_le_mult_iff)
 
-    txt \<open>@{text p} is absolutely homogeneous:\<close>
+    txt \<open>\<open>p\<close> is absolutely homogeneous:\<close>
 
     show "p (a \<cdot> x) = \<bar>a\<bar> * p x"
     proof -
@@ -396,7 +393,7 @@
       finally show ?thesis .
     qed
 
-    txt \<open>Furthermore, @{text p} is subadditive:\<close>
+    txt \<open>Furthermore, \<open>p\<close> is subadditive:\<close>
 
     show "p (x + y) \<le> p x + p y"
     proof -
@@ -411,7 +408,7 @@
     qed
   qed
 
-  txt \<open>@{text f} is bounded by @{text p}.\<close>
+  txt \<open>\<open>f\<close> is bounded by \<open>p\<close>.\<close>
 
   have "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
   proof
@@ -423,10 +420,10 @@
          OF F_norm, folded B_def fn_norm_def])
   qed
 
-  txt \<open>Using the fact that @{text p} is a seminorm and @{text f} is bounded
-    by @{text p} we can apply the Hahn-Banach Theorem for real vector
-    spaces. So @{text f} can be extended in a norm-preserving way to
-    some function @{text g} on the whole vector space @{text E}.\<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"
@@ -434,7 +431,7 @@
     and b: "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x"
     by (rule abs_Hahn_Banach [elim_format]) iprover
 
-  txt \<open>We furthermore have to show that @{text g} is also continuous:\<close>
+  txt \<open>We furthermore have to show that \<open>g\<close> is also continuous:\<close>
 
   have g_cont: "continuous E g norm" using linearformE
   proof
@@ -443,22 +440,21 @@
       by (simp only: p_def)
   qed
 
-  txt \<open>To complete the proof, we show that @{text "\<parallel>g\<parallel> = \<parallel>f\<parallel>"}.\<close>
+  txt \<open>To complete the proof, we show that \<open>\<parallel>g\<parallel> = \<parallel>f\<parallel>\<close>.\<close>
 
   have "\<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
   proof (rule order_antisym)
     txt \<open>
-      First we show @{text "\<parallel>g\<parallel> \<le> \<parallel>f\<parallel>"}.  The function norm @{text
-      "\<parallel>g\<parallel>"} is defined as the smallest @{text "c \<in> \<real>"} 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}
-      @{text "\<forall>x \<in> E. \<bar>g x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+      \<open>\<forall>x \<in> E. \<bar>g x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
       \end{tabular}
       \end{center}
       \noindent Furthermore holds
       \begin{center}
       \begin{tabular}{l}
-      @{text "\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
+      \<open>\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>\<close>
       \end{tabular}
       \end{center}
 \<close>
diff -r bf4969660913 -r a29295dac1ca src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Mon Nov 02 10:38:42 2015 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Mon Nov 02 11:10:28 2015 +0100
@@ -9,34 +9,32 @@
 begin
 
 text \<open>
-  In this section the following context is presumed.  Let @{text E} be
-  a real vector space with a seminorm @{text q} on @{text E}. @{text
-  F} is a subspace of @{text E} and @{text f} a linear function on
-  @{text F}. We consider a subspace @{text H} of @{text E} that is a
-  superspace of @{text F} and a linear form @{text h} on @{text
-  H}. @{text H} is a not equal to @{text E} and @{text "x\<^sub>0"} is
-  an element in @{text "E - H"}.  @{text H} is extended to the direct
-  sum @{text "H' = H + lin x\<^sub>0"}, so for any @{text "x \<in> H'"}
-  the decomposition of @{text "x = y + a \<cdot> x"} with @{text "y \<in> H"} is
-  unique. @{text h'} is defined on @{text H'} by @{text "h' x = h y +
-  a \<cdot> \<xi>"} for a certain @{text \<xi>}.
+  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 @{text h'} of
-  @{text h}.
+  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 @{text f} (see page \pageref{ex-xi-use}). It is a
-  consequence of the completeness of @{text \<real>}. To show
+  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}
-  @{text "\<exists>\<xi>. \<forall>y \<in> F. a y \<le> \<xi> \<and> \<xi> \<le> b y"}
+  \<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
   \begin{center}
   \begin{tabular}{l}
-  @{text "\<forall>u \<in> F. \<forall>v \<in> F. a u \<le> b v"}
+  \<open>\<forall>u \<in> F. \<forall>v \<in> F. a u \<le> b v\<close>
   \end{tabular}
   \end{center}
 \<close>
@@ -48,7 +46,7 @@
 proof -
   interpret vectorspace F by fact
   txt \<open>From the completeness of the reals follows:
-    The set @{text "S = {a u. u \<in> F}"} has a supremum, if it is
+    The set \<open>S = {a u. u \<in> F}\<close> has a supremum, if it is
     non-empty and has an upper bound.\<close>
 
   let ?S = "{a u | u. u \<in> F}"
@@ -86,9 +84,9 @@
 
 text \<open>
   \<^medskip>
-  The function @{text h'} is defined as a @{text "h' x = h y
-  + a \<cdot> \<xi>"} where @{text "x = y + a \<cdot> \<xi>"} is a linear extension of
-  @{text h} to @{text H'}.
+  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:
@@ -194,8 +192,8 @@
 
 text \<open>
   \<^medskip>
-  The linear extension @{text h'} of @{text h}
-  is bounded by the seminorm @{text p}.\<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) =
@@ -235,8 +233,8 @@
         also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp
         finally show ?thesis .
       next
-        txt \<open>In the case @{text "a < 0"}, we use @{text "a\<^sub>1"}
-          with @{text ya} taken as @{text "y / a"}:\<close>
+        txt \<open>In the case \<open>a < 0\<close>, we use \<open>a\<^sub>1\<close>
+          with \<open>ya\<close> taken as \<open>y / a\<close>:\<close>
         assume lz: "a < 0" then have nz: "a \<noteq> 0" by simp
         from a1 ay
         have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" ..
@@ -257,8 +255,8 @@
         finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
         then show ?thesis by simp
       next
-        txt \<open>In the case @{text "a > 0"}, we use @{text "a\<^sub>2"}
-          with @{text ya} taken as @{text "y / a"}:\<close>
+        txt \<open>In the case \<open>a > 0\<close>, we use \<open>a\<^sub>2\<close>
+          with \<open>ya\<close> taken as \<open>y / a\<close>:\<close>
         assume gz: "0 < a" then have nz: "a \<noteq> 0" by simp
         from a2 ay
         have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" ..
diff -r bf4969660913 -r a29295dac1ca src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Mon Nov 02 10:38:42 2015 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Mon Nov 02 11:10:28 2015 +0100
@@ -11,17 +11,17 @@
 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 @{text E} be a real vector space with a seminorm
-  @{text p} on @{text E}.  @{text F} is a subspace of @{text E} and
-  @{text f} a linear form on @{text F}. We consider a chain @{text c}
-  of norm-preserving extensions of @{text f}, such that @{text "\<Union>c =
-  graph H h"}.  We will show some properties about the limit function
-  @{text h}, i.e.\ the supremum of the chain @{text c}.
+  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 @{text c} be a chain of norm-preserving extensions of
-  the function @{text f} and let @{text "graph H h"} be the supremum
-  of @{text c}.  Every element in @{text H} is member of one of the
+  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>
 
@@ -57,11 +57,10 @@
 
 text \<open>
   \<^medskip>
-  Let @{text c} be a chain of norm-preserving extensions of
-  the function @{text f} and let @{text "graph H h"} be the supremum
-  of @{text c}.  Every element in the domain @{text H} of the supremum
-  function is member of the domain @{text H'} of some function @{text
-  h'}, such that @{text h} extends @{text h'}.
+  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':
@@ -86,10 +85,10 @@
 
 text \<open>
   \<^medskip>
-  Any two elements @{text x} and @{text y} in the domain
-  @{text H} of the supremum function @{text h} are both in the domain
-  @{text H'} of some function @{text h'}, such that @{text h} extends
-  @{text h'}.
+  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:
@@ -103,8 +102,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>@{text y} is in the domain @{text H''} of some function @{text h''},
-  such that @{text h} extends @{text h''}.\<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'"
@@ -114,8 +113,8 @@
       "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>@{text x} is in the domain @{text H'} of some function @{text h'},
-    such that @{text h} extends @{text h'}.\<close>
+  txt \<open>\<open>x\<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 x obtain H'' h'' where
       x_hx: "(x, h x) \<in> graph H'' h''"
@@ -125,9 +124,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 @{text h'} and @{text h''} are elements of the chain,
-    @{text h''} is an extension of @{text h'} or vice versa. Thus both
-    @{text x} and @{text y} are contained in the greater
+  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''"
@@ -160,7 +159,7 @@
 text \<open>
   \<^medskip>
   The relation induced by the graph of the supremum of a
-  chain @{text c} is definite, i.~e.~t is the graph of a function.
+  chain \<open>c\<close> is definite, i.~e.~t is the graph of a function.
 \<close>
 
 lemma sup_definite:
@@ -182,9 +181,8 @@
   then obtain H2 h2 where G2_rep: "G2 = graph H2 h2"
     unfolding M_def by blast
 
-  txt \<open>@{text "G\<^sub>1"} is contained in @{text "G\<^sub>2"}
-    or vice versa, since both @{text "G\<^sub>1"} and @{text
-    "G\<^sub>2"} are members of @{text c}. \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)
@@ -210,12 +208,12 @@
 
 text \<open>
   \<^medskip>
-  The limit function @{text h} is linear. Every element
-  @{text x} in the domain of @{text h} is in the domain of a function
-  @{text h'} in the chain of norm preserving extensions.  Furthermore,
-  @{text h} is an extension of @{text h'} so the function values of
-  @{text x} are identical for @{text h'} and @{text h}.  Finally, the
-  function @{text h'} is linear by construction of @{text M}.
+  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:
@@ -267,8 +265,8 @@
 text \<open>
   \<^medskip>
   The limit of a non-empty chain of norm preserving
-  extensions of @{text f} is an extension of @{text f}, since every
-  element of the chain is an extension of @{text f} and the supremum
+  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>
 
@@ -293,10 +291,10 @@
 
 text \<open>
   \<^medskip>
-  The domain @{text H} of the limit function is a superspace
-  of @{text F}, since @{text F} is a subset of @{text H}. The
-  existence of the @{text 0} element in @{text F} and the closure
-  properties follow from the fact that @{text F} is a vector space.
+  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>
 
 lemma sup_supF:
@@ -319,8 +317,8 @@
 
 text \<open>
   \<^medskip>
-  The domain @{text H} of the limit function is a subspace of
-  @{text E}.
+  The domain \<open>H\<close> of the limit function is a subspace of
+  \<open>E\<close>.
 \<close>
 
 lemma sup_subE:
@@ -376,8 +374,8 @@
 
 text \<open>
   \<^medskip>
-  The limit function is bounded by the norm @{text p} as
-  well, since all elements in the chain are bounded by @{text p}.
+  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:
@@ -399,13 +397,13 @@
 text \<open>
   \<^medskip>
   The following lemma is a property of linear forms on real
-  vector spaces. It will be used for the lemma @{text abs_Hahn_Banach}
+  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:
   \begin{center}
   \begin{tabular}{lll}
-  @{text "\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x"} & and &
-  @{text "\<forall>x \<in> H. h x \<le> p x"} \\
+  \<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>
diff -r bf4969660913 -r a29295dac1ca src/HOL/Hahn_Banach/Linearform.thy
--- a/src/HOL/Hahn_Banach/Linearform.thy	Mon Nov 02 10:38:42 2015 +0100
+++ b/src/HOL/Hahn_Banach/Linearform.thy	Mon Nov 02 11:10:28 2015 +0100
@@ -44,7 +44,7 @@
   finally show ?thesis by simp
 qed
 
-text \<open>Every linear form yields @{text 0} for the @{text 0} vector.\<close>
+text \<open>Every linear form yields \<open>0\<close> for the \<open>0\<close> vector.\<close>
 
 lemma (in linearform) zero [iff]:
   assumes "vectorspace V"
diff -r bf4969660913 -r a29295dac1ca src/HOL/Hahn_Banach/Normed_Space.thy
--- a/src/HOL/Hahn_Banach/Normed_Space.thy	Mon Nov 02 10:38:42 2015 +0100
+++ b/src/HOL/Hahn_Banach/Normed_Space.thy	Mon Nov 02 11:10:28 2015 +0100
@@ -11,7 +11,7 @@
 subsection \<open>Quasinorms\<close>
 
 text \<open>
-  A \<^emph>\<open>seminorm\<close> @{text "\<parallel>\<cdot>\<parallel>"} is a function on a real vector space
+  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>
@@ -57,8 +57,8 @@
 subsection \<open>Norms\<close>
 
 text \<open>
-  A \<^emph>\<open>norm\<close> @{text "\<parallel>\<cdot>\<parallel>"} is a seminorm that maps only the
-  @{text 0} vector to @{text 0}.
+  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 +
diff -r bf4969660913 -r a29295dac1ca src/HOL/Hahn_Banach/Subspace.thy
--- a/src/HOL/Hahn_Banach/Subspace.thy	Mon Nov 02 10:38:42 2015 +0100
+++ b/src/HOL/Hahn_Banach/Subspace.thy	Mon Nov 02 11:10:28 2015 +0100
@@ -11,8 +11,8 @@
 subsection \<open>Definition\<close>
 
 text \<open>
-  A non-empty subset @{text U} of a vector space @{text V} is a
-  \<^emph>\<open>subspace\<close> of @{text V}, iff @{text U} is closed under addition
+  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>
 
@@ -140,8 +140,8 @@
 subsection \<open>Linear closure\<close>
 
 text \<open>
-  The \<^emph>\<open>linear closure\<close> of a vector @{text x} is the set of all
-  scalar multiples of @{text x}.
+  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 +227,8 @@
 subsection \<open>Sum of two vectorspaces\<close>
 
 text \<open>
-  The \<^emph>\<open>sum\<close> of two vectorspaces @{text U} and @{text V} is the
-  set of all sums of elements from @{text U} and @{text V}.
+  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}"
@@ -246,7 +246,7 @@
     "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> u + v \<in> U + V"
   unfolding sum_def by blast
 
-text \<open>@{text U} is a subspace of @{text "U + V"}.\<close>
+text \<open>\<open>U\<close> is a subspace of \<open>U + V\<close>.\<close>
 
 lemma subspace_sum1 [iff]:
   assumes "vectorspace U" "vectorspace V"
@@ -329,11 +329,10 @@
 subsection \<open>Direct sums\<close>
 
 text \<open>
-  The sum of @{text U} and @{text V} is called \<^emph>\<open>direct\<close>, iff the
-  zero element is the only common element of @{text U} and @{text
-  V}. For every element @{text x} of the direct sum of @{text U} and
-  @{text V} the decomposition in @{text "x = u + v"} with
-  @{text "u \<in> U"} and @{text "v \<in> V"} 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:
@@ -380,9 +379,9 @@
 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 @{text "y + a \<cdot> x\<^sub>0"} of the direct sum of a
-  vectorspace @{text H} and the linear closure of @{text "x\<^sub>0"}
-  the components @{text "y \<in> H"} and @{text a} are uniquely
+  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>
 
@@ -437,10 +436,10 @@
 qed
 
 text \<open>
-  Since for any element @{text "y + a \<cdot> x'"} of the direct sum of a
-  vectorspace @{text H} and the linear closure of @{text x'} the
-  components @{text "y \<in> H"} and @{text a} are unique, it follows from
-  @{text "y \<in> H"} that @{text "a = 0"}.
+  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:
@@ -465,9 +464,9 @@
 qed
 
 text \<open>
-  The components @{text "y \<in> H"} and @{text a} in @{text "y + a \<cdot> x'"}
-  are unique, so the function @{text h'} defined by
-  @{text "h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>"} 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 bf4969660913 -r a29295dac1ca src/HOL/Hahn_Banach/Vector_Space.thy
--- a/src/HOL/Hahn_Banach/Vector_Space.thy	Mon Nov 02 10:38:42 2015 +0100
+++ b/src/HOL/Hahn_Banach/Vector_Space.thy	Mon Nov 02 11:10:28 2015 +0100
@@ -12,8 +12,8 @@
 
 text \<open>
   For the definition of real vector spaces a type @{typ 'a} of the
-  sort @{text "{plus, minus, zero}"} is considered, on which a real
-  scalar multiplication @{text \<cdot>} is declared.
+  sort \<open>{plus, minus, zero}\<close> is considered, on which a real
+  scalar multiplication \<open>\<cdot>\<close> is declared.
 \<close>
 
 consts
@@ -23,13 +23,12 @@
 subsection \<open>Vector space laws\<close>
 
 text \<open>
-  A \<^emph>\<open>vector space\<close> is a non-empty set @{text V} of elements from
-  @{typ 'a} with the following vector space laws: The set @{text V} is
+  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; @{text "- x"} is the inverse of @{text
-  x} w.~r.~t.~addition and @{text 0} is the neutral element of
+  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 @{text "1"} is
+  multiplication is associative and the real number \<open>1\<close> is
   the neutral element of scalar multiplication.
 \<close>
 
diff -r bf4969660913 -r a29295dac1ca src/HOL/Hahn_Banach/Zorn_Lemma.thy
--- a/src/HOL/Hahn_Banach/Zorn_Lemma.thy	Mon Nov 02 10:38:42 2015 +0100
+++ b/src/HOL/Hahn_Banach/Zorn_Lemma.thy	Mon Nov 02 11:10:28 2015 +0100
@@ -10,13 +10,12 @@
 
 text \<open>
   Zorn's Lemmas states: if every linear ordered subset of an ordered
-  set @{text S} has an upper bound in @{text S}, then there exists a
-  maximal element in @{text S}.  In our application, @{text S} is a
+  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 @{text S} is non-empty, it
-  suffices to show that for every non-empty chain @{text c} in @{text
-  S} the union of @{text c} also lies in @{text S}.
+  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:
@@ -30,14 +29,14 @@
     show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"
     proof cases
 
-      txt \<open>If @{text c} is an empty chain, then every element in
-        @{text S} is an upper bound of @{text c}.\<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 @{text c} is non-empty, then @{text "\<Union>c"} is an upper
-        bound of @{text c}, lying in @{text S}.\<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> {}"