# HG changeset patch
# User wenzelm
# Date 997212420 -7200
# Node ID d08d4e17a5f662246627517f9e891b48fc8d4585
# Parent  ba2c252b55adce15b6643b5451147fa5a6fd2fc7
tuned;

diff -r ba2c252b55ad -r d08d4e17a5f6 src/HOL/Real/HahnBanach/FunctionNorm.thy
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Tue Aug 07 19:29:08 2001 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Tue Aug 07 21:27:00 2001 +0200
@@ -10,10 +10,10 @@
 subsection {* Continuous linear forms*}
 
 text {*
-  A linear form @{text f} on a normed vector space @{text "(V, \\<parallel>\\<cdot>\\<parallel>)"}
+  A linear form @{text f} on a normed vector space @{text "(V, \<parallel>\<cdot>\<parallel>)"}
   is \emph{continuous}, 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>"}
+  @{text "\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
   \end{center}
   In our application no other functions than linear forms are
   considered, so we can define continuous linear forms as bounded
@@ -22,61 +22,58 @@
 
 constdefs
   is_continuous ::
-  "'a::{plus, minus, zero} set \\<Rightarrow> ('a \\<Rightarrow> real) \\<Rightarrow> ('a \\<Rightarrow> real) \\<Rightarrow> bool"
-  "is_continuous V norm f \\<equiv>
-    is_linearform V f \\<and> (\\<exists>c. \\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c * norm x)"
+  "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
+  "is_continuous V norm f \<equiv>
+    is_linearform V f \<and> (\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x)"
 
 lemma continuousI [intro]:
-  "is_linearform V f \\<Longrightarrow> (\\<And>x. x \\<in> V \\<Longrightarrow> \\<bar>f x\\<bar> \\<le> c * norm x)
-  \\<Longrightarrow> is_continuous V norm f"
-proof (unfold is_continuous_def, intro exI conjI ballI)
-  assume r: "\\<And>x. x \\<in> V \\<Longrightarrow> \\<bar>f x\\<bar> \\<le> c * norm x"
-  fix x assume "x \\<in> V" show "\\<bar>f x\\<bar> \\<le> c * norm x" by (rule r)
-qed
+  "is_linearform V f \<Longrightarrow> (\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * norm x)
+  \<Longrightarrow> is_continuous V norm f"
+  by (unfold is_continuous_def) blast
 
 lemma continuous_linearform [intro?]:
-  "is_continuous V norm f \\<Longrightarrow> is_linearform V f"
+  "is_continuous V norm f \<Longrightarrow> is_linearform V f"
   by (unfold is_continuous_def) blast
 
 lemma continuous_bounded [intro?]:
   "is_continuous V norm f
-  \\<Longrightarrow> \\<exists>c. \\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c * norm x"
+  \<Longrightarrow> \<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
   by (unfold is_continuous_def) blast
 
+
 subsection{* The norm of a linear form *}
 
-
 text {*
   The least real number @{text c} for which holds
   \begin{center}
-  @{text "\\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c \\<cdot> \\<parallel>x\\<parallel>"}
+  @{text "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
   \end{center}
   is called the \emph{norm} of @{text f}.
 
-  For non-trivial vector spaces @{text "V \\<noteq> {0}"} the norm can be
+  For non-trivial vector spaces @{text "V \<noteq> {0}"} the norm can be
   defined as
   \begin{center}
-  @{text "\\<parallel>f\\<parallel> = \<sup>x \\<noteq> 0. \\<bar>f x\\<bar> / \\<parallel>x\\<parallel>"}
+  @{text "\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>"}
   \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.
+  empty set. Since @{text \<real>} 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
+  element in this set. This element must be @{text "{} \<ge> 0"} so that
   @{text function_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 of are @{text "{} \\<ge> 0"}.
+  be @{text 0}, as all other elements of are @{text "{} \<ge> 0"}.
 
   Thus we define the set @{text B} the supremum is taken from as
   \begin{center}
-  @{text "{0} \\<union> {\\<bar>f x\\<bar> / \\<parallel>x\\<parallel>. x \\<noteq> 0 \\<and> x \\<in> F}"}
+  @{text "{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}"}
   \end{center}
 *}
 
 constdefs
-  B :: "'a set \\<Rightarrow> ('a \\<Rightarrow> real) \\<Rightarrow> ('a::{plus, minus, zero} \\<Rightarrow> real) \\<Rightarrow> real set"
-  "B V norm f \\<equiv>
-  {#0} \\<union> {\\<bar>f x\\<bar> * inverse (norm x) | x. x \\<noteq> 0 \\<and> x \\<in> V}"
+  B :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a::{plus, minus, zero} \<Rightarrow> real) \<Rightarrow> real set"
+  "B V norm f \<equiv>
+  {#0} \<union> {\<bar>f x\<bar> * inverse (norm x) | x. x \<noteq> 0 \<and> x \<in> V}"
 
 text {*
   @{text n} is the function norm of @{text f}, iff @{text n} is the
@@ -85,8 +82,8 @@
 
 constdefs
   is_function_norm ::
-  "('a::{minus,plus,zero} \\<Rightarrow> real) \\<Rightarrow> 'a set \\<Rightarrow> ('a \\<Rightarrow> real) \\<Rightarrow> real \\<Rightarrow> bool"
-  "is_function_norm f V norm fn \\<equiv> is_Sup UNIV (B V norm f) fn"
+  "('a::{minus,plus,zero} \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> bool"
+  "is_function_norm f V norm fn \<equiv> is_Sup UNIV (B V norm f) fn"
 
 text {*
   @{text function_norm} is equal to the supremum of @{text B}, if the
@@ -94,124 +91,124 @@
 *}
 
 constdefs
-  function_norm :: "('a::{minus,plus,zero} \\<Rightarrow> real) \\<Rightarrow> 'a set \\<Rightarrow> ('a \\<Rightarrow> real) \\<Rightarrow> real"
-  "function_norm f V norm \\<equiv> Sup UNIV (B V norm f)"
+  function_norm :: "('a::{minus,plus,zero} \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> real"
+  "function_norm f V norm \<equiv> Sup UNIV (B V norm f)"
 
 syntax
-  function_norm :: "('a \\<Rightarrow> real) \\<Rightarrow> 'a set \\<Rightarrow> ('a \\<Rightarrow> real) \\<Rightarrow> real"  ("\\<parallel>_\\<parallel>_,_")
+  function_norm :: "('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> real"  ("\<parallel>_\<parallel>_,_")
 
-lemma B_not_empty: "#0 \\<in> B V norm f"
+lemma B_not_empty: "#0 \<in> B V norm f"
   by (unfold B_def) blast
 
 text {*
   The following lemma states that every continuous linear form on a
-  normed space @{text "(V, \\<parallel>\\<cdot>\\<parallel>)"} has a function norm.
+  normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm.
 *}
 
 lemma ex_fnorm [intro?]:
-  "is_normed_vectorspace V norm \\<Longrightarrow> is_continuous V norm f
-     \\<Longrightarrow> is_function_norm f V norm \\<parallel>f\\<parallel>V,norm"
+  "is_normed_vectorspace V norm \<Longrightarrow> is_continuous V norm f
+     \<Longrightarrow> is_function_norm f V norm \<parallel>f\<parallel>V,norm"
 proof (unfold function_norm_def is_function_norm_def
   is_continuous_def Sup_def, elim conjE, rule someI2_ex)
   assume "is_normed_vectorspace V norm"
   assume "is_linearform V f"
-  and e: "\\<exists>c. \\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c * norm x"
+  and e: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
 
   txt {* The existence of the supremum is shown using the
   completeness of the reals. Completeness means, that
   every non-empty bounded set of reals has a
   supremum. *}
-  show  "\\<exists>a. is_Sup UNIV (B V norm f) a"
+  show  "\<exists>a. is_Sup UNIV (B V norm f) a"
   proof (unfold is_Sup_def, rule reals_complete)
 
     txt {* First we have to show that @{text B} is non-empty: *}
 
-    show "\\<exists>X. X \\<in> B V norm f"
+    show "\<exists>X. X \<in> B V norm f"
     proof
-      show "#0 \\<in> (B V norm f)" by (unfold B_def) blast
+      show "#0 \<in> (B V norm f)" by (unfold B_def) blast
     qed
 
     txt {* Then we have to show that @{text B} is bounded: *}
 
-    from e show "\\<exists>Y. isUb UNIV (B V norm f) Y"
+    from e show "\<exists>Y. isUb UNIV (B V norm f) Y"
     proof
 
       txt {* We know that @{text f} is bounded by some value @{text c}. *}
 
-      fix c assume a: "\\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c * norm x"
-      def b \\<equiv> "max c #0"
+      fix c assume a: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
+      def b \<equiv> "max c #0"
 
       show "?thesis"
       proof (intro exI isUbI setleI ballI, unfold B_def,
         elim UnE CollectE exE conjE singletonE)
 
         txt {* To proof the thesis, we have to show that there is some
-        constant @{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 for @{text "y \\<in> B"}.  If @{text "y = 0"} then
-        @{text "y \\<le> max c 0"}: *}
+        constant @{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 for @{text "y \<in> B"}.  If @{text "y = 0"} then
+        @{text "y \<le> max c 0"}: *}
 
         fix y assume "y = (#0::real)"
-        show "y \\<le> b" by (simp! add: le_maxI2)
+        show "y \<le> b" by (simp! add: le_maxI2)
 
-        txt {* The second case is @{text "y = \\<bar>f x\\<bar> / \\<parallel>x\\<parallel>"} for some
-        @{text "x \\<in> V"} with @{text "x \\<noteq> 0"}. *}
+        txt {* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
+        @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *}
 
       next
         fix x y
-        assume "x \\<in> V"  "x \\<noteq> 0"
+        assume "x \<in> V"  "x \<noteq> 0"
 
         txt {* The thesis follows by a short calculation using the
         fact that @{text f} is bounded. *}
 
-        assume "y = \\<bar>f x\\<bar> * inverse (norm x)"
-        also have "... \\<le> c * norm x * inverse (norm x)"
+        assume "y = \<bar>f x\<bar> * inverse (norm x)"
+        also have "... \<le> c * norm x * inverse (norm x)"
         proof (rule real_mult_le_le_mono2)
-          show "#0 \\<le> inverse (norm x)"
+          show "#0 \<le> inverse (norm x)"
             by (rule order_less_imp_le, rule real_inverse_gt_zero1,
                 rule normed_vs_norm_gt_zero)
-          from a show "\\<bar>f x\\<bar> \\<le> c * norm x" ..
+          from a show "\<bar>f x\<bar> \<le> c * norm x" ..
         qed
         also have "... = c * (norm x * inverse (norm x))"
           by (rule real_mult_assoc)
         also have "(norm x * inverse (norm x)) = (#1::real)"
         proof (rule real_mult_inv_right1)
-          show nz: "norm x \\<noteq> #0"
+          show nz: "norm x \<noteq> #0"
             by (rule not_sym, rule lt_imp_not_eq,
               rule normed_vs_norm_gt_zero)
         qed
-        also have "c * ... \\<le> b " by (simp! add: le_maxI1)
-        finally show "y \\<le> b" .
+        also have "c * ... \<le> b " by (simp! add: le_maxI1)
+        finally show "y \<le> b" .
       qed simp
     qed
   qed
 qed
 
-text {* The norm of a continuous function is always @{text "\\<ge> 0"}. *}
+text {* The norm of a continuous function is always @{text "\<ge> 0"}. *}
 
 lemma fnorm_ge_zero [intro?]:
-  "is_continuous V norm f \\<Longrightarrow> is_normed_vectorspace V norm
-   \\<Longrightarrow> #0 \\<le> \\<parallel>f\\<parallel>V,norm"
+  "is_continuous V norm f \<Longrightarrow> is_normed_vectorspace V norm
+   \<Longrightarrow> #0 \<le> \<parallel>f\<parallel>V,norm"
 proof -
   assume c: "is_continuous V norm f"
      and n: "is_normed_vectorspace V norm"
 
   txt {* 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
+  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. *}
 
   show ?thesis
   proof (unfold function_norm_def, rule sup_ub1)
-    show "\\<forall>x \\<in> (B V norm f). #0 \\<le> x"
+    show "\<forall>x \<in> (B V norm f). #0 \<le> x"
     proof (intro ballI, unfold B_def,
            elim UnE singletonE CollectE exE conjE)
       fix x r
-      assume "x \\<in> V"  "x \\<noteq> 0"
-        and r: "r = \\<bar>f x\\<bar> * inverse (norm x)"
+      assume "x \<in> V"  "x \<noteq> 0"
+        and r: "r = \<bar>f x\<bar> * inverse (norm x)"
 
-      have ge: "#0 \\<le> \\<bar>f x\\<bar>" by (simp! only: abs_ge_zero)
-      have "#0 \\<le> inverse (norm x)"
+      have ge: "#0 \<le> \<bar>f x\<bar>" by (simp! only: abs_ge_zero)
+      have "#0 \<le> inverse (norm x)"
         by (rule order_less_imp_le, rule real_inverse_gt_zero1, rule)(***
         proof (rule order_less_imp_le);
           show "#0 < inverse (norm x)";
@@ -219,34 +216,34 @@
             show "#0 < norm x"; ..;
           qed;
         qed; ***)
-      with ge show "#0 \\<le> r"
+      with ge show "#0 \<le> r"
        by (simp only: r, rule real_le_mult_order1a)
     qed (simp!)
 
     txt {* Since @{text f} is continuous the function norm exists: *}
 
-    have "is_function_norm f V norm \\<parallel>f\\<parallel>V,norm" ..
+    have "is_function_norm f V norm \<parallel>f\<parallel>V,norm" ..
     thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
       by (unfold is_function_norm_def function_norm_def)
 
     txt {* @{text B} is non-empty by construction: *}
 
-    show "#0 \\<in> B V norm f" by (rule B_not_empty)
+    show "#0 \<in> B V norm f" by (rule B_not_empty)
   qed
 qed
 
 text {*
   \medskip The fundamental property of function norms is:
   \begin{center}
-  @{text "\\<bar>f x\\<bar> \\<le> \\<parallel>f\\<parallel> \\<cdot> \\<parallel>x\\<parallel>"}
+  @{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
   \end{center}
 *}
 
 lemma norm_fx_le_norm_f_norm_x:
-  "is_continuous V norm f \\<Longrightarrow> is_normed_vectorspace V norm \\<Longrightarrow> x \\<in> V
-    \\<Longrightarrow> \\<bar>f x\\<bar> \\<le> \\<parallel>f\\<parallel>V,norm * norm x"
+  "is_continuous V norm f \<Longrightarrow> is_normed_vectorspace V norm \<Longrightarrow> x \<in> V
+    \<Longrightarrow> \<bar>f x\<bar> \<le> \<parallel>f\<parallel>V,norm * norm x"
 proof -
-  assume "is_normed_vectorspace V norm"  "x \\<in> V"
+  assume "is_normed_vectorspace V norm"  "x \<in> V"
   and c: "is_continuous V norm f"
   have v: "is_vectorspace V" ..
 
@@ -260,46 +257,46 @@
     @{text "f 0 = 0"}. *}
 
     assume "x = 0"
-    have "\\<bar>f x\\<bar> = \\<bar>f 0\\<bar>" by (simp!)
+    have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by (simp!)
     also from v continuous_linearform have "f 0 = #0" ..
     also note abs_zero
-    also have "#0 \\<le> \\<parallel>f\\<parallel>V,norm * norm x"
+    also have "#0 \<le> \<parallel>f\<parallel>V,norm * norm x"
     proof (rule real_le_mult_order1a)
-      show "#0 \\<le> \\<parallel>f\\<parallel>V,norm" ..
-      show "#0 \\<le> norm x" ..
+      show "#0 \<le> \<parallel>f\<parallel>V,norm" ..
+      show "#0 \<le> norm x" ..
     qed
     finally
-    show "\\<bar>f x\\<bar> \\<le> \\<parallel>f\\<parallel>V,norm * norm x" .
+    show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>V,norm * norm x" .
 
   next
-    assume "x \\<noteq> 0"
+    assume "x \<noteq> 0"
     have n: "#0 < norm x" ..
-    hence nz: "norm x \\<noteq> #0"
+    hence nz: "norm x \<noteq> #0"
       by (simp only: lt_imp_not_eq)
 
-    txt {* For the case @{text "x \\<noteq> 0"} we derive the following fact
+    txt {* For the case @{text "x \<noteq> 0"} we derive the following fact
     from the definition of the function norm:*}
 
-    have l: "\\<bar>f x\\<bar> * inverse (norm x) \\<le> \\<parallel>f\\<parallel>V,norm"
+    have l: "\<bar>f x\<bar> * inverse (norm x) \<le> \<parallel>f\<parallel>V,norm"
     proof (unfold function_norm_def, rule sup_ub)
       from ex_fnorm [OF _ c]
       show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
          by (simp! add: is_function_norm_def function_norm_def)
-      show "\\<bar>f x\\<bar> * inverse (norm x) \\<in> B V norm f"
+      show "\<bar>f x\<bar> * inverse (norm x) \<in> B V norm f"
         by (unfold B_def, intro UnI2 CollectI exI [of _ x]
             conjI, simp)
     qed
 
     txt {* The thesis now follows by a short calculation: *}
 
-    have "\\<bar>f x\\<bar> = \\<bar>f x\\<bar> * #1" by (simp!)
+    have "\<bar>f x\<bar> = \<bar>f x\<bar> * #1" by (simp!)
     also from nz have "#1 = inverse (norm x) * norm x"
       by (simp add: real_mult_inv_left1)
-    also have "\\<bar>f x\\<bar> * ... = \\<bar>f x\\<bar> * inverse (norm x) * norm x"
+    also have "\<bar>f x\<bar> * ... = \<bar>f x\<bar> * inverse (norm x) * norm x"
       by (simp! add: real_mult_assoc)
-    also from n l have "... \\<le> \\<parallel>f\\<parallel>V,norm * norm x"
+    also from n l have "... \<le> \<parallel>f\<parallel>V,norm * norm x"
       by (simp add: real_mult_le_le_mono2)
-    finally show "\\<bar>f x\\<bar> \\<le> \\<parallel>f\\<parallel>V,norm * norm x" .
+    finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>V,norm * norm x" .
   qed
 qed
 
@@ -307,72 +304,72 @@
   \medskip 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>"}
+  @{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
   \end{center}
 *}
 
 lemma fnorm_le_ub:
-  "is_continuous V norm f \\<Longrightarrow> is_normed_vectorspace V norm \\<Longrightarrow>
-     \\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c * norm x \\<Longrightarrow> #0 \\<le> c
-  \\<Longrightarrow> \\<parallel>f\\<parallel>V,norm \\<le> c"
+  "is_continuous V norm f \<Longrightarrow> is_normed_vectorspace V norm \<Longrightarrow>
+     \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x \<Longrightarrow> #0 \<le> c
+  \<Longrightarrow> \<parallel>f\<parallel>V,norm \<le> c"
 proof (unfold function_norm_def)
   assume "is_normed_vectorspace V norm"
   assume c: "is_continuous V norm f"
-  assume fb: "\\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c * norm x"
-    and "#0 \\<le> c"
+  assume fb: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
+    and "#0 \<le> c"
 
-  txt {* Suppose the inequation holds for some @{text "c \\<ge> 0"}.  If
+  txt {* Suppose the inequation holds for some @{text "c \<ge> 0"}.  If
   @{text c} is an upper bound of @{text B}, then @{text c} is greater
   than the function norm since the function norm is the least upper
   bound.  *}
 
-  show "Sup UNIV (B V norm f) \\<le> c"
+  show "Sup UNIV (B V norm f) \<le> c"
   proof (rule sup_le_ub)
     from ex_fnorm [OF _ c]
     show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
       by (simp! add: is_function_norm_def function_norm_def)
 
     txt {* @{text c} is an upper bound of @{text B}, i.e. every
-    @{text "y \\<in> B"} is less than @{text c}. *}
+    @{text "y \<in> B"} is less than @{text c}. *}
 
     show "isUb UNIV (B V norm f) c"
     proof (intro isUbI setleI ballI)
-      fix y assume "y \\<in> B V norm f"
-      thus le: "y \\<le> c"
+      fix y assume "y \<in> B V norm f"
+      thus le: "y \<le> c"
       proof (unfold B_def, elim UnE CollectE exE conjE singletonE)
 
-       txt {* The first case for @{text "y \\<in> B"} is @{text "y = 0"}. *}
+       txt {* The first case for @{text "y \<in> B"} is @{text "y = 0"}. *}
 
         assume "y = #0"
-        show "y \\<le> c" by (blast!)
+        show "y \<le> c" by (blast!)
 
-        txt{* The second case is @{text "y = \\<bar>f x\\<bar> / \\<parallel>x\\<parallel>"} for some
-        @{text "x \\<in> V"} with @{text "x \\<noteq> 0"}. *}
+        txt{* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
+        @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *}
 
       next
         fix x
-        assume "x \\<in> V"  "x \\<noteq> 0"
+        assume "x \<in> V"  "x \<noteq> 0"
 
         have lz: "#0 < norm x"
           by (simp! add: normed_vs_norm_gt_zero)
 
-        have nz: "norm x \\<noteq> #0"
+        have nz: "norm x \<noteq> #0"
         proof (rule not_sym)
-          from lz show "#0 \\<noteq> norm x"
+          from lz show "#0 \<noteq> norm x"
             by (simp! add: order_less_imp_not_eq)
         qed
 
         from lz have "#0 < inverse (norm x)"
           by (simp! add: real_inverse_gt_zero1)
-        hence inverse_gez: "#0 \\<le> inverse (norm x)"
+        hence inverse_gez: "#0 \<le> inverse (norm x)"
           by (rule order_less_imp_le)
 
-        assume "y = \\<bar>f x\\<bar> * inverse (norm x)"
-        also from inverse_gez have "... \\<le> c * norm x * inverse (norm x)"
+        assume "y = \<bar>f x\<bar> * inverse (norm x)"
+        also from inverse_gez have "... \<le> c * norm x * inverse (norm x)"
           proof (rule real_mult_le_le_mono2)
-            show "\\<bar>f x\\<bar> \\<le> c * norm x" by (rule bspec)
+            show "\<bar>f x\<bar> \<le> c * norm x" by (rule bspec)
           qed
-        also have "... \\<le> c" by (simp add: nz real_mult_assoc)
+        also have "... \<le> c" by (simp add: nz real_mult_assoc)
         finally show ?thesis .
       qed
     qed blast
diff -r ba2c252b55ad -r d08d4e17a5f6 src/HOL/Real/HahnBanach/FunctionOrder.thy
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Tue Aug 07 19:29:08 2001 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Tue Aug 07 21:27:00 2001 +0200
@@ -27,7 +27,7 @@
   "graph F f \<equiv> {(x, f x) | x. x \<in> F}"
 
 lemma graphI [intro?]: "x \<in> F \<Longrightarrow> (x, f x) \<in> graph F f"
-  by (unfold graph_def, intro CollectI exI) blast
+  by (unfold graph_def) blast
 
 lemma graphI2 [intro?]: "x \<in> F \<Longrightarrow> \<exists>t\<in> (graph F f). t = (x, f x)"
   by (unfold graph_def) blast
diff -r ba2c252b55ad -r d08d4e17a5f6 src/HOL/Real/HahnBanach/VectorSpace.thy
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Tue Aug 07 19:29:08 2001 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Tue Aug 07 21:27:00 2001 +0200
@@ -146,14 +146,10 @@
 proof -
   assume "is_vectorspace V"
   have "V \<noteq> {}" ..
-  hence "\<exists>x. x \<in> V" by blast
-  thus ?thesis
-  proof
-    fix x assume "x \<in> V"
-    have "0 = x - x" by (simp!)
-    also have "... \<in> V" by (simp! only: vs_diff_closed)
-    finally show ?thesis .
-  qed
+  then obtain x where "x \<in> V" by blast
+  have "0 = x - x" by (simp!)
+  also have "... \<in> V" by (simp! only: vs_diff_closed)
+  finally show ?thesis .
 qed
 
 lemma vs_add_zero_left [simp]: