# HG changeset patch
# User wenzelm
# Date 965255662 -7200
# Node ID 3324cbbecef8ac787ea83b4a786665e5f1dc9c99
# Parent  50ec59aff3897dcf520b8451b6b4f6a603ef749f
tuned;

diff -r 50ec59aff389 -r 3324cbbecef8 src/HOL/Real/HahnBanach/Aux.thy
--- a/src/HOL/Real/HahnBanach/Aux.thy	Wed Aug 02 19:40:14 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Aux.thy	Thu Aug 03 00:34:22 2000 +0200
@@ -17,22 +17,22 @@
 text_raw {* \medskip *}
 text{* Lemmas about sets. *}
 
-lemma Int_singletonD: "[| A \\<inter> B = {v}; x \\<in> A; x \\<in> B |] ==> x = v"
+lemma Int_singletonD: "[| A \<inter> B = {v}; x \<in> A; x \<in> B |] ==> x = v"
   by (fast elim: equalityE)
 
-lemma set_less_imp_diff_not_empty: "H < E ==> \\<exists>x0 \\<in> E. x0 \\<notin> H"
+lemma set_less_imp_diff_not_empty: "H < E ==> \<exists>x0 \<in> E. x0 \<notin> H"
   by (force simp add: psubset_eq)
 
 text_raw {* \medskip *}
 text{* Some lemmas about orders. *}
 
-lemma lt_imp_not_eq: "x < (y::'a::order) ==> x \\<noteq> y"
+lemma lt_imp_not_eq: "x < (y::'a::order) ==> x \<noteq> y"
   by (simp add: order_less_le)
 
 lemma le_noteq_imp_less: 
-  "[| x <= (r::'a::order); x \\<noteq> r |] ==> x < r"
+  "[| x <= (r::'a::order); x \<noteq> r |] ==> x < r"
 proof -
-  assume "x <= r" and ne:"x \\<noteq> r"
+  assume "x <= r" and ne:"x \<noteq> r"
   hence "x < r | x = r" by (simp add: order_le_less)
   with ne show ?thesis by simp
 qed
@@ -103,10 +103,10 @@
   thus ?thesis by simp
 qed
 
-lemma real_mult_inv_right1: "x \\<noteq> #0 ==> x*rinv(x) = #1"
+lemma real_mult_inv_right1: "x \<noteq> #0 ==> x*rinv(x) = #1"
   by simp
 
-lemma real_mult_inv_left1: "x \\<noteq> #0 ==> rinv(x) * x = #1"
+lemma real_mult_inv_left1: "x \<noteq> #0 ==> rinv(x) * x = #1"
   by simp
 
 lemma real_le_mult_order1a: 
diff -r 50ec59aff389 -r 3324cbbecef8 src/HOL/Real/HahnBanach/Bounds.thy
--- a/src/HOL/Real/HahnBanach/Bounds.thy	Wed Aug 02 19:40:14 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Bounds.thy	Thu Aug 03 00:34:22 2000 +0200
@@ -11,13 +11,13 @@
 
 constdefs
   is_LowerBound :: "('a::order) set => 'a set => 'a => bool"
-  "is_LowerBound A B == \\<lambda>x. x \\<in> A \\<and> (\\<forall>y \\<in> B. x <= y)"
+  "is_LowerBound A B == \<lambda>x. x \<in> A \<and> (\<forall>y \<in> B. x <= y)"
    
   LowerBounds :: "('a::order) set => 'a set => 'a set"
   "LowerBounds A B == Collect (is_LowerBound A B)"
 
   is_UpperBound :: "('a::order) set => 'a set => 'a => bool"
-  "is_UpperBound A B == \\<lambda>x. x \\<in> A \\<and> (\\<forall>y \\<in> B. y <= x)"
+  "is_UpperBound A B == \<lambda>x. x \<in> A \<and> (\<forall>y \<in> B. y <= x)"
  
   UpperBounds :: "('a::order) set => 'a set => 'a set"
   "UpperBounds A B == Collect (is_UpperBound A B)"
@@ -33,9 +33,9 @@
     ("(3LOWER'_BOUNDS _./ _)" 10)
 
 translations
-  "UPPER_BOUNDS x:A. P" == "UpperBounds A (Collect (\\<lambda>x. P))"
+  "UPPER_BOUNDS x:A. P" == "UpperBounds A (Collect (\<lambda>x. P))"
   "UPPER_BOUNDS x. P" == "UPPER_BOUNDS x:UNIV. P"
-  "LOWER_BOUNDS x:A. P" == "LowerBounds A (Collect (\\<lambda>x. P))"
+  "LOWER_BOUNDS x:A. P" == "LowerBounds A (Collect (\<lambda>x. P))"
   "LOWER_BOUNDS x. P" == "LOWER_BOUNDS x:UNIV. P"
 
 
@@ -86,7 +86,7 @@
 (*<*)
 constdefs
   is_Inf :: "('a::order) set => 'a set => 'a => bool"
-  "is_Inf A B x == x \\<in> A \\<and>  is_Greatest (LowerBounds A B) x"
+  "is_Inf A B x == x \<in> A \<and>  is_Greatest (LowerBounds A B) x"
 
   Inf :: "('a::order) set => 'a set => 'a"
   "Inf A B == Eps (is_Inf A B)"
@@ -102,9 +102,9 @@
     ("(3INF _./ _)" 10)
 
 translations
-  "SUP x:A. P" == "Sup A (Collect (\\<lambda>x. P))"
+  "SUP x:A. P" == "Sup A (Collect (\<lambda>x. P))"
   "SUP x. P" == "SUP x:UNIV. P"
-  "INF x:A. P" == "Inf A (Collect (\\<lambda>x. P))"
+  "INF x:A. P" == "Inf A (Collect (\<lambda>x. P))"
   "INF x. P" == "INF x:UNIV. P"
 (*>*)
 text{* The supremum of $B$ is less than any upper bound
@@ -115,16 +115,16 @@
 
 text {* The supremum $B$ is an upper bound for $B$. *}
 
-lemma sup_ub: "y \\<in> B ==> is_Sup A B s ==> y <= s"
+lemma sup_ub: "y \<in> B ==> is_Sup A B s ==> y <= s"
   by (unfold is_Sup_def, rule isLubD2)
 
 text{* The supremum of a non-empty set $B$ is greater
 than a lower bound of $B$. *}
 
 lemma sup_ub1: 
-  "[| \\<forall>y \\<in> B. a <= y; is_Sup A B s; x \\<in> B |] ==> a <= s"
+  "[| \<forall>y \<in> B. a <= y; is_Sup A B s; x \<in> B |] ==> a <= s"
 proof - 
-  assume "\\<forall>y \\<in> B. a <= y" "is_Sup A B s" "x \\<in> B"
+  assume "\<forall>y \<in> B. a <= y" "is_Sup A B s" "x \<in> B"
   have "a <= x" by (rule bspec)
   also have "x <= s" by (rule sup_ub)
   finally show "a <= s" .
diff -r 50ec59aff389 -r 3324cbbecef8 src/HOL/Real/HahnBanach/FunctionNorm.thy
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Wed Aug 02 19:40:14 2000 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Thu Aug 03 00:34:22 2000 +0200
@@ -20,14 +20,14 @@
   is_continuous ::
   "['a::{plus, minus, zero} set, 'a => real, 'a => real] => bool" 
   "is_continuous V norm f == 
-    is_linearform V f \\<and> (\\<exists>c. \\<forall>x \\<in> V. |f x| <= c * norm x)"
+    is_linearform V f \<and> (\<exists>c. \<forall>x \<in> V. |f x| <= c * norm x)"
 
 lemma continuousI [intro]: 
-  "[| is_linearform V f; !! x. x \\<in> V ==> |f x| <= c * norm x |] 
+  "[| is_linearform V f; !! x. x \<in> V ==> |f x| <= c * norm x |] 
   ==> is_continuous V norm f"
 proof (unfold is_continuous_def, intro exI conjI ballI)
-  assume r: "!! x. x \\<in> V ==> |f x| <= c * norm x" 
-  fix x assume "x \\<in> V" show "|f x| <= c * norm x" by (rule r)
+  assume r: "!! x. x \<in> V ==> |f x| <= c * norm x" 
+  fix x assume "x \<in> V" show "|f x| <= c * norm x" by (rule r)
 qed
   
 lemma continuous_linearform [intro?]: 
@@ -36,7 +36,7 @@
 
 lemma continuous_bounded [intro?]:
   "is_continuous V norm f 
-  ==> \\<exists>c. \\<forall>x \\<in> V. |f x| <= c * norm x"
+  ==> \<exists>c. \<forall>x \<in> V. |f x| <= c * norm x"
   by (unfold is_continuous_def) force
 
 subsection{* The norm of a linear form *}
@@ -66,7 +66,7 @@
 constdefs
   B :: "[ 'a set, 'a => real, 'a::{plus, minus, zero} => real ] => real set"
   "B V norm f == 
-  {#0} \\<union> {|f x| * rinv (norm x) | x. x \\<noteq> 0 \\<and> x \\<in> V}"
+  {#0} \<union> {|f x| * rinv (norm x) | x. x \<noteq> 0 \<and> x \<in> V}"
 
 text{* $n$ is the function norm of $f$, iff 
 $n$ is the supremum of $B$. 
@@ -85,9 +85,9 @@
   "function_norm f V norm == Sup UNIV (B V norm f)"
 
 syntax   
-  function_norm :: " ['a => real, 'a set, 'a => real] => real" ("\\<parallel>_\\<parallel>_,_")
+  function_norm :: " ['a => real, 'a set, 'a => real] => 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, force)
 
 text {* The following lemma states that every continuous linear form
@@ -95,35 +95,35 @@
 
 lemma ex_fnorm [intro?]: 
   "[| is_normed_vectorspace V norm; is_continuous V norm f|]
-     ==> is_function_norm f V norm \\<parallel>f\\<parallel>V,norm" 
+     ==> 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 selectI2EX)
   assume "is_normed_vectorspace V norm"
   assume "is_linearform V f" 
-  and e: "\\<exists>c. \\<forall>x \\<in> V. |f x| <= c * norm x"
+  and e: "\<exists>c. \<forall>x \<in> V. |f x| <= 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 $B$ is non-empty: *} 
 
-    show "\\<exists>X. X \\<in> B V norm f" 
+    show "\<exists>X. X \<in> B V norm f" 
     proof (intro exI)
-      show "#0 \\<in> (B V norm f)" by (unfold B_def, force)
+      show "#0 \<in> (B V norm f)" by (unfold B_def, force)
     qed
 
     txt {* Then we have to show that $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 $f$ is bounded by some value $c$. *}  
   
-      fix c assume a: "\\<forall>x \\<in> V. |f x| <= c * norm x"
+      fix c assume a: "\<forall>x \<in> V. |f x| <= c * norm x"
       def b == "max c #0"
 
       show "?thesis"
@@ -144,7 +144,7 @@
 
       next
 	fix x y
-        assume "x \\<in> V" "x \\<noteq> 0" (***
+        assume "x \<in> V" "x \<noteq> 0" (***
 
          have ge: "#0 <= rinv (norm x)";
           by (rule real_less_imp_le, rule real_rinv_gt_zero, 
@@ -155,11 +155,11 @@
               show "#0 < norm x"; ..;
             qed;
           qed; *** )
-        have nz: "norm x \\<noteq> #0" 
+        have nz: "norm x \<noteq> #0" 
           by (rule not_sym, rule lt_imp_not_eq, 
               rule normed_vs_norm_gt_zero) (***
           proof (rule not_sym);
-            show "#0 \\<noteq> norm x"; 
+            show "#0 \<noteq> norm x"; 
             proof (rule lt_imp_not_eq);
               show "#0 < norm x"; ..;
             qed;
@@ -180,7 +180,7 @@
           by (rule real_mult_assoc)
         also have "(norm x * rinv (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
@@ -195,7 +195,7 @@
 
 lemma fnorm_ge_zero [intro?]: 
   "[| is_continuous V norm f; is_normed_vectorspace V norm |]
-   ==> #0 <= \\<parallel>f\\<parallel>V,norm"
+   ==> #0 <= \<parallel>f\<parallel>V,norm"
 proof -
   assume c: "is_continuous V norm f" 
      and n: "is_normed_vectorspace V norm"
@@ -206,11 +206,11 @@
 
   show ?thesis 
   proof (unfold function_norm_def, rule sup_ub1)
-    show "\\<forall>x \\<in> (B V norm f). #0 <= x" 
+    show "\<forall>x \<in> (B V norm f). #0 <= x" 
     proof (intro ballI, unfold B_def,
            elim UnE singletonE CollectE exE conjE) 
       fix x r
-      assume "x \\<in> V" "x \\<noteq> 0" 
+      assume "x \<in> V" "x \<noteq> 0" 
         and r: "r = |f x| * rinv (norm x)"
 
       have ge: "#0 <= |f x|" by (simp! only: abs_ge_zero)
@@ -228,13 +228,13 @@
 
     txt {* Since $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 {* $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
   
@@ -245,10 +245,10 @@
 *}
 
 lemma norm_fx_le_norm_f_norm_x: 
-  "[| is_continuous V norm f; is_normed_vectorspace V norm; x \\<in> V |] 
-    ==> |f x| <= \\<parallel>f\\<parallel>V,norm * norm x"
+  "[| is_continuous V norm f; is_normed_vectorspace V norm; x \<in> V |] 
+    ==> |f x| <= \<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" ..
 
@@ -265,29 +265,29 @@
     have "|f x| = |f 0|" by (simp!)
     also from v continuous_linearform have "f 0 = #0" ..
     also note abs_zero
-    also have "#0 <= \\<parallel>f\\<parallel>V,norm * norm x"
+    also have "#0 <= \<parallel>f\<parallel>V,norm * norm x"
     proof (rule real_le_mult_order1a)
-      show "#0 <= \\<parallel>f\\<parallel>V,norm" ..
+      show "#0 <= \<parallel>f\<parallel>V,norm" ..
       show "#0 <= norm x" ..
     qed
     finally 
-    show "|f x| <= \\<parallel>f\\<parallel>V,norm * norm x" .
+    show "|f x| <= \<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 $x\neq \zero$ we derive the following
     fact from the definition of the function norm:*}
 
-    have l: "|f x| * rinv (norm x) <= \\<parallel>f\\<parallel>V,norm"
+    have l: "|f x| * rinv (norm x) <= \<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 "|f x| * rinv (norm x) \\<in> B V norm f" 
+      show "|f x| * rinv (norm x) \<in> B V norm f" 
         by (unfold B_def, intro UnI2 CollectI exI [of _ x]
             conjI, simp)
     qed
@@ -299,9 +299,9 @@
       by (simp add: real_mult_inv_left1)
     also have "|f x| * ... = |f x| * rinv (norm x) * norm x"
       by (simp! add: real_mult_assoc)
-    also from n l have "... <= \\<parallel>f\\<parallel>V,norm * norm x"
+    also from n l have "... <= \<parallel>f\<parallel>V,norm * norm x"
       by (simp add: real_mult_le_le_mono2)
-    finally show "|f x| <= \\<parallel>f\\<parallel>V,norm * norm x" .
+    finally show "|f x| <= \<parallel>f\<parallel>V,norm * norm x" .
   qed
 qed
 
@@ -314,12 +314,12 @@
 
 lemma fnorm_le_ub: 
   "[| is_continuous V norm f; is_normed_vectorspace V norm; 
-     \\<forall>x \\<in> V. |f x| <= c * norm x; #0 <= c |]
-  ==> \\<parallel>f\\<parallel>V,norm <= c"
+     \<forall>x \<in> V. |f x| <= c * norm x; #0 <= c |]
+  ==> \<parallel>f\<parallel>V,norm <= 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. |f x| <= c * norm x"
+  assume fb: "\<forall>x \<in> V. |f x| <= c * norm x"
     and "#0 <= c"
 
   txt {* Suppose the inequation holds for some $c\geq 0$.
@@ -339,7 +339,7 @@
 
     show "isUb UNIV (B V norm f) c"  
     proof (intro isUbI setleI ballI)
-      fix y assume "y \\<in> B V norm f"
+      fix y assume "y \<in> B V norm f"
       thus le: "y <= c"
       proof (unfold B_def, elim UnE CollectE exE conjE singletonE)
 
@@ -354,14 +354,14 @@
 
       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
             
diff -r 50ec59aff389 -r 3324cbbecef8 src/HOL/Real/HahnBanach/FunctionOrder.thy
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Wed Aug 02 19:40:14 2000 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Thu Aug 03 00:34:22 2000 +0200
@@ -22,18 +22,18 @@
 
 constdefs
   graph :: "['a set, 'a => real] => 'a graph "
-  "graph F f == {(x, f x) | x. x \\<in> F}" 
+  "graph F f == {(x, f x) | x. x \<in> F}" 
 
-lemma graphI [intro?]: "x \\<in> F ==> (x, f x) \\<in> graph F f"
+lemma graphI [intro?]: "x \<in> F ==> (x, f x) \<in> graph F f"
   by (unfold graph_def, intro CollectI exI) force
 
-lemma graphI2 [intro?]: "x \\<in> F ==> \\<exists>t\\<in> (graph F f). t = (x, f x)"
+lemma graphI2 [intro?]: "x \<in> F ==> \<exists>t\<in> (graph F f). t = (x, f x)"
   by (unfold graph_def, force)
 
-lemma graphD1 [intro?]: "(x, y) \\<in> graph F f ==> x \\<in> F"
+lemma graphD1 [intro?]: "(x, y) \<in> graph F f ==> x \<in> F"
   by (unfold graph_def, elim CollectE exE) force
 
-lemma graphD2 [intro?]: "(x, y) \\<in> graph H h ==> y = h x"
+lemma graphD2 [intro?]: "(x, y) \<in> graph H h ==> y = h x"
   by (unfold graph_def, elim CollectE exE) force 
 
 subsection {* Functions ordered by domain extension *}
@@ -42,12 +42,12 @@
 $h$ is a subset of the graph of $h'$.*}
 
 lemma graph_extI: 
-  "[| !! x. x \\<in> H ==> h x = h' x; H <= H'|]
+  "[| !! x. x \<in> H ==> h x = h' x; H <= H'|]
   ==> graph H h <= graph H' h'"
   by (unfold graph_def, force)
 
 lemma graph_extD1 [intro?]: 
-  "[| graph H h <= graph H' h'; x \\<in> H |] ==> h x = h' x"
+  "[| graph H h <= graph H' h'; x \<in> H |] ==> h x = h' x"
   by (unfold graph_def, force)
 
 lemma graph_extD2 [intro?]: 
@@ -61,26 +61,26 @@
 
 constdefs
   domain :: "'a graph => 'a set" 
-  "domain g == {x. \\<exists>y. (x, y) \\<in> g}"
+  "domain g == {x. \<exists>y. (x, y) \<in> g}"
 
   funct :: "'a graph => ('a => real)"
-  "funct g == \\<lambda>x. (SOME y. (x, y) \\<in> g)"
+  "funct g == \<lambda>x. (SOME y. (x, y) \<in> g)"
 
 
 text {* The following lemma states that $g$ is the graph of a function
 if the relation induced by $g$ is unique. *}
 
 lemma graph_domain_funct: 
-  "(!!x y z. (x, y) \\<in> g ==> (x, z) \\<in> g ==> z = y) 
+  "(!!x y z. (x, y) \<in> g ==> (x, z) \<in> g ==> z = y) 
   ==> graph (domain g) (funct g) = g"
 proof (unfold domain_def funct_def graph_def, auto)
-  fix a b assume "(a, b) \\<in> g"
-  show "(a, SOME y. (a, y) \\<in> g) \\<in> g" by (rule selectI2)
-  show "\\<exists>y. (a, y) \\<in> g" ..
-  assume uniq: "!!x y z. (x, y) \\<in> g ==> (x, z) \\<in> g ==> z = y"
-  show "b = (SOME y. (a, y) \\<in> g)"
+  fix a b assume "(a, b) \<in> g"
+  show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule selectI2)
+  show "\<exists>y. (a, y) \<in> g" ..
+  assume uniq: "!!x y z. (x, y) \<in> g ==> (x, z) \<in> g ==> z = y"
+  show "b = (SOME y. (a, y) \<in> g)"
   proof (rule select_equality [RS sym])
-    fix y assume "(a, y) \\<in> g" show "y = b" by (rule uniq)
+    fix y assume "(a, y) \<in> g" show "y = b" by (rule uniq)
   qed
 qed
 
@@ -98,37 +98,37 @@
     "['a::{plus, minus, zero} set, 'a  => real, 'a set, 'a => real] 
     => 'a graph set"
     "norm_pres_extensions E p F f 
-    == {g. \\<exists>H h. graph H h = g 
-                \\<and> is_linearform H h 
-                \\<and> is_subspace H E
-                \\<and> is_subspace F H
-                \\<and> graph F f <= graph H h
-                \\<and> (\\<forall>x \\<in> H. h x <= p x)}"
+    == {g. \<exists>H h. graph H h = g 
+                \<and> is_linearform H h 
+                \<and> is_subspace H E
+                \<and> is_subspace F H
+                \<and> graph F f <= graph H h
+                \<and> (\<forall>x \<in> H. h x <= p x)}"
                        
 lemma norm_pres_extension_D:  
-  "g \\<in> norm_pres_extensions E p F f
-  ==> \\<exists>H h. graph H h = g 
-            \\<and> is_linearform H h 
-            \\<and> is_subspace H E
-            \\<and> is_subspace F H
-            \\<and> graph F f <= graph H h
-            \\<and> (\\<forall>x \\<in> H. h x <= p x)"
+  "g \<in> norm_pres_extensions E p F f
+  ==> \<exists>H h. graph H h = g 
+            \<and> is_linearform H h 
+            \<and> is_subspace H E
+            \<and> is_subspace F H
+            \<and> graph F f <= graph H h
+            \<and> (\<forall>x \<in> H. h x <= p x)"
   by (unfold norm_pres_extensions_def) force
 
 lemma norm_pres_extensionI2 [intro]:  
   "[| is_linearform H h; is_subspace H E; is_subspace F H;
-  graph F f <= graph H h; \\<forall>x \\<in> H. h x <= p x |]
-  ==> (graph H h \\<in> norm_pres_extensions E p F f)"
+  graph F f <= graph H h; \<forall>x \<in> H. h x <= p x |]
+  ==> (graph H h \<in> norm_pres_extensions E p F f)"
  by (unfold norm_pres_extensions_def) force
 
 lemma norm_pres_extensionI [intro]:  
-  "\\<exists>H h. graph H h = g 
-         \\<and> is_linearform H h    
-         \\<and> is_subspace H E
-         \\<and> is_subspace F H
-         \\<and> graph F f <= graph H h
-         \\<and> (\\<forall>x \\<in> H. h x <= p x)
-  ==> g \\<in> norm_pres_extensions E p F f"
+  "\<exists>H h. graph H h = g 
+         \<and> is_linearform H h    
+         \<and> is_subspace H E
+         \<and> is_subspace F H
+         \<and> graph F f <= graph H h
+         \<and> (\<forall>x \<in> H. h x <= p x)
+  ==> g \<in> norm_pres_extensions E p F f"
   by (unfold norm_pres_extensions_def) force
 
 end
\ No newline at end of file
diff -r 50ec59aff389 -r 3324cbbecef8 src/HOL/Real/HahnBanach/HahnBanach.thy
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Wed Aug 02 19:40:14 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Aug 03 00:34:22 2000 +0200
@@ -64,37 +64,37 @@
 
 theorem HahnBanach:
   "[| is_vectorspace E; is_subspace F E; is_seminorm E p;
-  is_linearform F f; \\<forall>x \\<in> F. f x <= p x |] 
-  ==> \\<exists>h. is_linearform E h \\<and> (\\<forall>x \\<in> F. h x = f x)
-        \\<and> (\\<forall>x \\<in> E. h x <= p x)"   
+  is_linearform F f; \<forall>x \<in> F. f x <= p x |] 
+  ==> \<exists>h. is_linearform E h \<and> (\<forall>x \<in> F. h x = f x)
+        \<and> (\<forall>x \<in> E. h x <= p x)"   
     -- {* Let $E$ be a vector space, $F$ a subspace of $E$, $p$ a seminorm on $E$, *}
     -- {* and $f$ a linear form on $F$ such that $f$ is bounded by $p$, *}
     -- {* then $f$ can be extended to a linear form $h$ on $E$ in a norm-preserving way. \skp *}
 proof -
   assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p" 
-   and "is_linearform F f" "\\<forall>x \\<in> F. f x <= p x"
+   and "is_linearform F f" "\<forall>x \<in> F. f x <= p x"
   -- {* Assume the context of the theorem. \skp *}
   def M == "norm_pres_extensions E p F f"
   -- {* Define $M$ as the set of all norm-preserving extensions of $F$. \skp *}
   {
-    fix c assume "c \\<in> chain M" "\\<exists>x. x \\<in> c"
-    have "\\<Union>c \\<in> M"
+    fix c assume "c \<in> chain M" "\<exists>x. x \<in> c"
+    have "\<Union>c \<in> M"
     -- {* Show that every non-empty chain $c$ of $M$ has an upper bound in $M$: *}
     -- {* $\Union c$ is greater than any element of the chain $c$, so it suffices to show $\Union c \in M$. *}
     proof (unfold M_def, rule norm_pres_extensionI)
-      show "\\<exists>H h. graph H h = \\<Union>c
-              \\<and> is_linearform H h 
-              \\<and> is_subspace H E 
-              \\<and> is_subspace F H 
-              \\<and> graph F f \\<subseteq> graph H h
-              \\<and> (\\<forall>x \\<in> H. h x <= p x)"
+      show "\<exists>H h. graph H h = \<Union>c
+              \<and> is_linearform H h 
+              \<and> is_subspace H E 
+              \<and> is_subspace F H 
+              \<and> graph F f \<subseteq> graph H h
+              \<and> (\<forall>x \<in> H. h x <= p x)"
       proof (intro exI conjI)
-        let ?H = "domain (\\<Union>c)"
-        let ?h = "funct (\\<Union>c)"
+        let ?H = "domain (\<Union>c)"
+        let ?h = "funct (\<Union>c)"
 
-        show a: "graph ?H ?h = \\<Union>c" 
+        show a: "graph ?H ?h = \<Union>c" 
         proof (rule graph_domain_funct)
-          fix x y z assume "(x, y) \\<in> \\<Union>c" "(x, z) \\<in> \\<Union>c"
+          fix x y z assume "(x, y) \<in> \<Union>c" "(x, z) \<in> \<Union>c"
           show "z = y" by (rule sup_definite)
         qed
         show "is_linearform ?H ?h" 
@@ -103,40 +103,40 @@
           by (rule sup_subE, rule a) (simp!)+
         show "is_subspace F ?H" 
           by (rule sup_supF, rule a) (simp!)+
-        show "graph F f \\<subseteq> graph ?H ?h" 
+        show "graph F f \<subseteq> graph ?H ?h" 
           by (rule sup_ext, rule a) (simp!)+
-        show "\\<forall>x \\<in> ?H. ?h x <= p x" 
+        show "\<forall>x \<in> ?H. ?h x <= p x" 
           by (rule sup_norm_pres, rule a) (simp!)+
       qed
     qed
 
   }
-  hence "\\<exists>g \\<in> M. \\<forall>x \\<in> M. g \\<subseteq> x --> g = x" 
+  hence "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x --> g = x" 
   -- {* With Zorn's Lemma we can conclude that there is a maximal element in $M$.\skp *}
   proof (rule Zorn's_Lemma)
     -- {* We show that $M$ is non-empty: *}
-    have "graph F f \\<in> norm_pres_extensions E p F f"
+    have "graph F f \<in> norm_pres_extensions E p F f"
     proof (rule norm_pres_extensionI2)
       have "is_vectorspace F" ..
       thus "is_subspace F F" ..
     qed (blast!)+ 
-    thus "graph F f \\<in> M" by (simp!)
+    thus "graph F f \<in> M" by (simp!)
   qed
   thus ?thesis
   proof
-    fix g assume "g \\<in> M" "\\<forall>x \\<in> M. g \\<subseteq> x --> g = x"
+    fix g assume "g \<in> M" "\<forall>x \<in> M. g \<subseteq> x --> g = x"
     -- {* We consider such a maximal element $g \in M$. \skp *}
     obtain H h where "graph H h = g" "is_linearform H h" 
-      "is_subspace H E" "is_subspace F H" "graph F f \\<subseteq> graph H h" 
-      "\\<forall>x \\<in> H. h x <= p x" 
+      "is_subspace H E" "is_subspace F H" "graph F f \<subseteq> graph H h" 
+      "\<forall>x \<in> H. h x <= p x" 
       -- {* $g$ is a norm-preserving extension of $f$, in other words: *}
       -- {* $g$ is the graph of some linear form $h$ defined on a subspace $H$ of $E$, *}
       -- {* and $h$ is an extension of $f$ that is again bounded by $p$. \skp *}
     proof -
-      have "\\<exists>H h. graph H h = g \\<and> is_linearform H h 
-        \\<and> is_subspace H E \\<and> is_subspace F H
-        \\<and> graph F f \\<subseteq> graph H h
-        \\<and> (\\<forall>x \\<in> H. h x <= p x)" 
+      have "\<exists>H h. graph H h = g \<and> is_linearform H h 
+        \<and> is_subspace H E \<and> is_subspace F H
+        \<and> graph F f \<subseteq> graph H h
+        \<and> (\<forall>x \<in> H. h x <= p x)" 
         by (simp! add: norm_pres_extension_D)
       thus ?thesis by (elim exE conjE) rule
     qed
@@ -144,39 +144,39 @@
     have "H = E"
     -- {* We show that $h$ is defined on whole $E$ by classical contradiction. \skp *} 
     proof (rule classical)
-      assume "H \\<noteq> E"
+      assume "H \<noteq> E"
       -- {* Assume $h$ is not defined on whole $E$. Then show that $h$ can be extended *}
       -- {* in a norm-preserving way to a function $h'$ with the graph $g'$. \skp *}
-      have "\\<exists>g' \\<in> M. g \\<subseteq> g' \\<and> g \\<noteq> g'"
+      have "\<exists>g' \<in> M. g \<subseteq> g' \<and> g \<noteq> g'"
       proof -
-        obtain x' where "x' \\<in> E" "x' \\<notin> H" 
+        obtain x' where "x' \<in> E" "x' \<notin> H" 
         -- {* Pick $x' \in E \setminus H$. \skp *}
         proof -
-          have "\\<exists>x' \\<in> E. x' \\<notin> H"
+          have "\<exists>x' \<in> E. x' \<notin> H"
           proof (rule set_less_imp_diff_not_empty)
-            have "H \\<subseteq> E" ..
-            thus "H \\<subset> E" ..
+            have "H \<subseteq> E" ..
+            thus "H \<subset> E" ..
           qed
           thus ?thesis by blast
         qed
-        have x': "x' \\<noteq> 0"
+        have x': "x' \<noteq> 0"
         proof (rule classical)
           presume "x' = 0"
-          with h have "x' \\<in> H" by simp
+          with h have "x' \<in> H" by simp
           thus ?thesis by contradiction
         qed blast
         def H' == "H + lin x'"
         -- {* Define $H'$ as the direct sum of $H$ and the linear closure of $x'$. \skp *}
-        obtain xi where "\\<forall>y \\<in> H. - p (y + x') - h y <= xi 
-                          \\<and> xi <= p (y + x') - h y" 
+        obtain xi where "\<forall>y \<in> H. - p (y + x') - h y <= xi 
+                          \<and> xi <= p (y + x') - h y" 
         -- {* Pick a real number $\xi$ that fulfills certain inequations; this will *}
         -- {* be used to establish that $h'$ is a norm-preserving extension of $h$. 
            \label{ex-xi-use}\skp *}
         proof -
-          from h have "\\<exists>xi. \\<forall>y \\<in> H. - p (y + x') - h y <= xi 
-                          \\<and> xi <= p (y + x') - h y" 
+          from h have "\<exists>xi. \<forall>y \<in> H. - p (y + x') - h y <= xi 
+                          \<and> xi <= p (y + x') - h y" 
           proof (rule ex_xi)
-            fix u v assume "u \\<in> H" "v \\<in> H"
+            fix u v assume "u \<in> H" "v \<in> H"
             from h have "h v - h u = h (v - u)"
               by (simp! add: linearform_diff)
             also have "... <= p (v - u)"
@@ -197,25 +197,25 @@
           thus ?thesis by rule rule
         qed
 
-        def h' == "\\<lambda>x. let (y,a) = SOME (y,a). x = y + a \\<cdot> x' \\<and> y \\<in> H
+        def h' == "\<lambda>x. let (y,a) = SOME (y,a). x = y + a \<cdot> x' \<and> y \<in> H
                        in (h y) + a * xi"
         -- {* Define the extension $h'$ of $h$ to $H'$ using $\xi$. \skp *}
         show ?thesis
         proof
-          show "g \\<subseteq> graph H' h' \\<and> g \\<noteq> graph H' h'" 
+          show "g \<subseteq> graph H' h' \<and> g \<noteq> graph H' h'" 
           -- {* Show that $h'$ is an extension of $h$ \dots \skp *}
           proof
-            show "g \\<subseteq> graph H' h'"
+            show "g \<subseteq> graph H' h'"
             proof -
-              have  "graph H h \\<subseteq> graph H' h'"
+              have  "graph H h \<subseteq> graph H' h'"
               proof (rule graph_extI)
-                fix t assume "t \\<in> H" 
-                have "(SOME (y, a). t = y + a \\<cdot> x' \\<and> y \\<in> H)
+                fix t assume "t \<in> H" 
+                have "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H)
                      = (t, #0)"
                   by (rule decomp_H'_H) (assumption+, rule x')
                 thus "h t = h' t" by (simp! add: Let_def)
               next
-                show "H \\<subseteq> H'"
+                show "H \<subseteq> H'"
                 proof (rule subspace_subset)
                   show "is_subspace H H'"
                   proof (unfold H'_def, rule subspace_vs_sum1)
@@ -226,29 +226,29 @@
               qed 
               thus ?thesis by (simp!)
             qed
-            show "g \\<noteq> graph H' h'"
+            show "g \<noteq> graph H' h'"
             proof -
-              have "graph H h \\<noteq> graph H' h'"
+              have "graph H h \<noteq> graph H' h'"
               proof
                 assume e: "graph H h = graph H' h'"
-                have "x' \\<in> H'" 
+                have "x' \<in> H'" 
                 proof (unfold H'_def, rule vs_sumI)
                   show "x' = 0 + x'" by (simp!)
-                  from h show "0 \\<in> H" ..
-                  show "x' \\<in> lin x'" by (rule x_lin_x)
+                  from h show "0 \<in> H" ..
+                  show "x' \<in> lin x'" by (rule x_lin_x)
                 qed
-                hence "(x', h' x') \\<in> graph H' h'" ..
-                with e have "(x', h' x') \\<in> graph H h" by simp
-                hence "x' \\<in> H" ..
+                hence "(x', h' x') \<in> graph H' h'" ..
+                with e have "(x', h' x') \<in> graph H h" by simp
+                hence "x' \<in> H" ..
                 thus False by contradiction
               qed
               thus ?thesis by (simp!)
             qed
           qed
-          show "graph H' h' \\<in> M" 
+          show "graph H' h' \<in> M" 
           -- {* and $h'$ is norm-preserving. \skp *}
           proof -
-            have "graph H' h' \\<in> norm_pres_extensions E p F f"
+            have "graph H' h' \<in> norm_pres_extensions E p F f"
             proof (rule norm_pres_extensionI2)
               show "is_linearform H' h'"
                 by (rule h'_lf) (simp! add: x')+
@@ -261,47 +261,47 @@
               finally (subspace_trans [OF _ h]) 
               show f_h': "is_subspace F H'" .
             
-              show "graph F f \\<subseteq> graph H' h'"
+              show "graph F f \<subseteq> graph H' h'"
               proof (rule graph_extI)
-                fix x assume "x \\<in> F"
+                fix x assume "x \<in> F"
                 have "f x = h x" ..
                 also have " ... = h x + #0 * xi" by simp
                 also 
                 have "... = (let (y,a) = (x, #0) in h y + a * xi)"
                   by (simp add: Let_def)
                 also have 
-                  "(x, #0) = (SOME (y, a). x = y + a \\<cdot> x' \\<and> y \\<in> H)"
+                  "(x, #0) = (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)"
                   by (rule decomp_H'_H [RS sym]) (simp! add: x')+
                 also have 
-                  "(let (y,a) = (SOME (y,a). x = y + a \\<cdot> x' \\<and> y \\<in> H)
+                  "(let (y,a) = (SOME (y,a). x = y + a \<cdot> x' \<and> y \<in> H)
                     in h y + a * xi) = h' x" by (simp!)
                 finally show "f x = h' x" .
               next
-                from f_h' show "F \\<subseteq> H'" ..
+                from f_h' show "F \<subseteq> H'" ..
               qed
             
-              show "\\<forall>x \\<in> H'. h' x <= p x"
+              show "\<forall>x \<in> H'. h' x <= p x"
                 by (rule h'_norm_pres) (assumption+, rule x')
             qed
-            thus "graph H' h' \\<in> M" by (simp!)
+            thus "graph H' h' \<in> M" by (simp!)
           qed
         qed
       qed
-      hence "\\<not> (\\<forall>x \\<in> M. g \\<subseteq> x --> g = x)" by simp
+      hence "\<not> (\<forall>x \<in> M. g \<subseteq> x --> g = x)" by simp
 	-- {* So the graph $g$ of $h$ cannot be maximal. Contradiction! \skp *}
       thus "H = E" by contradiction
     qed
-    thus "\\<exists>h. is_linearform E h \\<and> (\\<forall>x \\<in> F. h x = f x) 
-      \\<and> (\\<forall>x \\<in> E. h x <= p x)" 
+    thus "\<exists>h. is_linearform E h \<and> (\<forall>x \<in> F. h x = f x) 
+      \<and> (\<forall>x \<in> E. h x <= p x)" 
     proof (intro exI conjI)
       assume eq: "H = E"
       from eq show "is_linearform E h" by (simp!)
-      show "\\<forall>x \\<in> F. h x = f x"
+      show "\<forall>x \<in> F. h x = f x"
       proof
-	fix x assume "x \\<in> F" have "f x = h x " ..
+	fix x assume "x \<in> F" have "f x = h x " ..
 	thus "h x = f x" ..
       qed
-      from eq show "\\<forall>x \\<in> E. h x <= p x" by (force!)
+      from eq show "\<forall>x \<in> E. h x <= p x" by (force!)
     qed
   qed
 qed
@@ -322,21 +322,21 @@
 
 theorem abs_HahnBanach:
 "[| is_vectorspace E; is_subspace F E; is_linearform F f; 
-is_seminorm E p; \\<forall>x \\<in> F. |f x| <= p x |]
-==> \\<exists>g. is_linearform E g \\<and> (\\<forall>x \\<in> F. g x = f x)
- \\<and> (\\<forall>x \\<in> E. |g x| <= p x)"
+is_seminorm E p; \<forall>x \<in> F. |f x| <= p x |]
+==> \<exists>g. is_linearform E g \<and> (\<forall>x \<in> F. g x = f x)
+ \<and> (\<forall>x \<in> E. |g x| <= p x)"
 proof -
 assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p" 
-"is_linearform F f"  "\\<forall>x \\<in> F. |f x| <= p x"
-have "\\<forall>x \\<in> F. f x <= p x"  by (rule abs_ineq_iff [RS iffD1])
-hence "\\<exists>g. is_linearform E g \\<and> (\\<forall>x \\<in> F. g x = f x) 
-          \\<and> (\\<forall>x \\<in> E. g x <= p x)"
+"is_linearform F f"  "\<forall>x \<in> F. |f x| <= p x"
+have "\<forall>x \<in> F. f x <= p x"  by (rule abs_ineq_iff [RS iffD1])
+hence "\<exists>g. is_linearform E g \<and> (\<forall>x \<in> F. g x = f x) 
+          \<and> (\<forall>x \<in> E. g x <= p x)"
 by (simp! only: HahnBanach)
 thus ?thesis 
 proof (elim exE conjE)
-fix g assume "is_linearform E g" "\\<forall>x \\<in> F. g x = f x" 
-              "\\<forall>x \\<in> E. g x <= p x"
-hence "\\<forall>x \\<in> E. |g x| <= p x"
+fix g assume "is_linearform E g" "\<forall>x \<in> F. g x = f x" 
+              "\<forall>x \<in> E. g x <= p x"
+hence "\<forall>x \<in> E. |g x| <= p x"
   by (simp! add: abs_ineq_iff [OF subspace_refl])
 thus ?thesis by (intro exI conjI)
 qed
@@ -351,10 +351,10 @@
 theorem norm_HahnBanach:
 "[| is_normed_vectorspace E norm; is_subspace F E; 
 is_linearform F f; is_continuous F norm f |] 
-==> \\<exists>g. is_linearform E g
-     \\<and> is_continuous E norm g 
-     \\<and> (\\<forall>x \\<in> F. g x = f x) 
-     \\<and> \\<parallel>g\\<parallel>E,norm = \\<parallel>f\\<parallel>F,norm"
+==> \<exists>g. is_linearform E g
+     \<and> is_continuous E norm g 
+     \<and> (\<forall>x \<in> F. g x = f x) 
+     \<and> \<parallel>g\<parallel>E,norm = \<parallel>f\<parallel>F,norm"
 proof -
 assume e_norm: "is_normed_vectorspace E norm"
 assume f: "is_subspace F E" "is_linearform F f"
@@ -368,32 +368,32 @@
 \end{matharray}
 *}
 
-def p == "\\<lambda>x. \\<parallel>f\\<parallel>F,norm * norm x"
+def p == "\<lambda>x. \<parallel>f\<parallel>F,norm * norm x"
 
 txt{* $p$ is a seminorm on $E$: *}
 
 have q: "is_seminorm E p"
 proof
-fix x y a assume "x \\<in> E" "y \\<in> E"
+fix x y a assume "x \<in> E" "y \<in> E"
 
 txt{* $p$ is positive definite: *}
 
 show "#0 <= p x"
 proof (unfold p_def, rule real_le_mult_order1a)
-  from f_cont f_norm show "#0 <= \\<parallel>f\\<parallel>F,norm" ..
+  from f_cont f_norm show "#0 <= \<parallel>f\<parallel>F,norm" ..
   show "#0 <= norm x" ..
 qed
 
 txt{* $p$ is absolutely homogenous: *}
 
-show "p (a \\<cdot> x) = |a| * p x"
+show "p (a \<cdot> x) = |a| * p x"
 proof - 
-  have "p (a \\<cdot> x) = \\<parallel>f\\<parallel>F,norm * norm (a \\<cdot> x)"
+  have "p (a \<cdot> x) = \<parallel>f\<parallel>F,norm * norm (a \<cdot> x)"
     by (simp!)
-  also have "norm (a \\<cdot> x) = |a| * norm x" 
+  also have "norm (a \<cdot> x) = |a| * norm x" 
     by (rule normed_vs_norm_abs_homogenous)
-  also have "\\<parallel>f\\<parallel>F,norm * ( |a| * norm x ) 
-    = |a| * (\\<parallel>f\\<parallel>F,norm * norm x)"
+  also have "\<parallel>f\<parallel>F,norm * ( |a| * norm x ) 
+    = |a| * (\<parallel>f\<parallel>F,norm * norm x)"
     by (simp! only: real_mult_left_commute)
   also have "... = |a| * p x" by (simp!)
   finally show ?thesis .
@@ -403,16 +403,16 @@
 
 show "p (x + y) <= p x + p y"
 proof -
-  have "p (x + y) = \\<parallel>f\\<parallel>F,norm * norm (x + y)"
+  have "p (x + y) = \<parallel>f\<parallel>F,norm * norm (x + y)"
     by (simp!)
   also 
-  have "... <= \\<parallel>f\\<parallel>F,norm * (norm x + norm y)"
+  have "... <= \<parallel>f\<parallel>F,norm * (norm x + norm y)"
   proof (rule real_mult_le_le_mono1a)
-    from f_cont f_norm show "#0 <= \\<parallel>f\\<parallel>F,norm" ..
+    from f_cont f_norm show "#0 <= \<parallel>f\<parallel>F,norm" ..
     show "norm (x + y) <= norm x + norm y" ..
   qed
-  also have "... = \\<parallel>f\\<parallel>F,norm * norm x 
-                    + \\<parallel>f\\<parallel>F,norm * norm y"
+  also have "... = \<parallel>f\<parallel>F,norm * norm x 
+                    + \<parallel>f\<parallel>F,norm * norm y"
     by (simp! only: real_add_mult_distrib2)
   finally show ?thesis by (simp!)
 qed
@@ -420,9 +420,9 @@
 
 txt{* $f$ is bounded by $p$. *} 
 
-have "\\<forall>x \\<in> F. |f x| <= p x"
+have "\<forall>x \<in> F. |f x| <= p x"
 proof
-fix x assume "x \\<in> F"
+fix x assume "x \<in> F"
  from f_norm show "|f x| <= p x" 
    by (simp! add: norm_fx_le_norm_f_norm_x)
 qed
@@ -434,20 +434,20 @@
 $g$ on the whole vector space $E$. *}
 
 with e f q 
-have "\\<exists>g. is_linearform E g \\<and> (\\<forall>x \\<in> F. g x = f x) 
-        \\<and> (\\<forall>x \\<in> E. |g x| <= p x)"
+have "\<exists>g. is_linearform E g \<and> (\<forall>x \<in> F. g x = f x) 
+        \<and> (\<forall>x \<in> E. |g x| <= p x)"
 by (simp! add: abs_HahnBanach)
 
 thus ?thesis
 proof (elim exE conjE) 
 fix g
-assume "is_linearform E g" and a: "\\<forall>x \\<in> F. g x = f x" 
-   and b: "\\<forall>x \\<in> E. |g x| <= p x"
+assume "is_linearform E g" and a: "\<forall>x \<in> F. g x = f x" 
+   and b: "\<forall>x \<in> E. |g x| <= p x"
 
-show "\\<exists>g. is_linearform E g 
-        \\<and> is_continuous E norm g 
-        \\<and> (\\<forall>x \\<in> F. g x = f x) 
-        \\<and> \\<parallel>g\\<parallel>E,norm = \\<parallel>f\\<parallel>F,norm"
+show "\<exists>g. is_linearform E g 
+        \<and> is_continuous E norm g 
+        \<and> (\<forall>x \<in> F. g x = f x) 
+        \<and> \<parallel>g\<parallel>E,norm = \<parallel>f\<parallel>F,norm"
 proof (intro exI conjI)
 
 txt{* We furthermore have to show that 
@@ -455,15 +455,15 @@
 
   show g_cont: "is_continuous E norm g"
   proof
-    fix x assume "x \\<in> E"
-    with b show "|g x| <= \\<parallel>f\\<parallel>F,norm * norm x"
+    fix x assume "x \<in> E"
+    with b show "|g x| <= \<parallel>f\<parallel>F,norm * norm x"
       by (simp add: p_def) 
   qed 
 
   txt {* To complete the proof, we show that 
   $\fnorm g = \fnorm f$. \label{order_antisym} *}
 
-  show "\\<parallel>g\\<parallel>E,norm = \\<parallel>f\\<parallel>F,norm"
+  show "\<parallel>g\<parallel>E,norm = \<parallel>f\<parallel>F,norm"
     (is "?L = ?R")
   proof (rule order_antisym)
 
@@ -478,36 +478,36 @@
     \end{matharray}
     *}
  
-    have "\\<forall>x \\<in> E. |g x| <= \\<parallel>f\\<parallel>F,norm * norm x"
+    have "\<forall>x \<in> E. |g x| <= \<parallel>f\<parallel>F,norm * norm x"
     proof
-      fix x assume "x \\<in> E" 
-      show "|g x| <= \\<parallel>f\\<parallel>F,norm * norm x"
+      fix x assume "x \<in> E" 
+      show "|g x| <= \<parallel>f\<parallel>F,norm * norm x"
         by (simp!)
     qed
 
     with g_cont e_norm show "?L <= ?R"
     proof (rule fnorm_le_ub)
-      from f_cont f_norm show "#0 <= \\<parallel>f\\<parallel>F,norm" ..
+      from f_cont f_norm show "#0 <= \<parallel>f\<parallel>F,norm" ..
     qed
 
     txt{* The other direction is achieved by a similar 
     argument. *}
 
-    have "\\<forall>x \\<in> F. |f x| <= \\<parallel>g\\<parallel>E,norm * norm x"
+    have "\<forall>x \<in> F. |f x| <= \<parallel>g\<parallel>E,norm * norm x"
     proof
-      fix x assume "x \\<in> F" 
+      fix x assume "x \<in> F" 
       from a have "g x = f x" ..
       hence "|f x| = |g x|" by simp
       also from g_cont
-      have "... <= \\<parallel>g\\<parallel>E,norm * norm x"
+      have "... <= \<parallel>g\<parallel>E,norm * norm x"
       proof (rule norm_fx_le_norm_f_norm_x)
-        show "x \\<in> E" ..
+        show "x \<in> E" ..
       qed
-      finally show "|f x| <= \\<parallel>g\\<parallel>E,norm * norm x" .
+      finally show "|f x| <= \<parallel>g\<parallel>E,norm * norm x" .
     qed 
     thus "?R <= ?L" 
     proof (rule fnorm_le_ub [OF f_cont f_norm])
-      from g_cont show "#0 <= \\<parallel>g\\<parallel>E,norm" ..
+      from g_cont show "#0 <= \<parallel>g\<parallel>E,norm" ..
     qed
   qed
 qed
diff -r 50ec59aff389 -r 3324cbbecef8 src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Wed Aug 02 19:40:14 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Thu Aug 03 00:34:22 2000 +0200
@@ -35,42 +35,42 @@
 \end{matharray} *};
 
 lemma ex_xi: 
-  "[| is_vectorspace F; !! u v. [| u \\<in> F; v \\<in> F |] ==> a u <= b v |]
-  ==> \\<exists>xi::real. \\<forall>y \\<in> F. a y <= xi \\<and> xi <= b y"; 
+  "[| is_vectorspace F; !! u v. [| u \<in> F; v \<in> F |] ==> a u <= b v |]
+  ==> \<exists>xi::real. \<forall>y \<in> F. a y <= xi \<and> xi <= b y"; 
 proof -;
   assume vs: "is_vectorspace F";
-  assume r: "(!! u v. [| u \\<in> F; v \\<in> F |] ==> a u <= (b v::real))";
+  assume r: "(!! u v. [| u \<in> F; v \<in> F |] ==> a u <= (b v::real))";
 
   txt {* From the completeness of the reals follows:
   The set $S = \{a\: u\dt\: u\in F\}$ has a supremum, if
   it is non-empty and has an upper bound. *};
 
-  let ?S = "{a u :: real | u. u \\<in> F}";
+  let ?S = "{a u :: real | u. u \<in> F}";
 
-  have "\\<exists>xi. isLub UNIV ?S xi";  
+  have "\<exists>xi. isLub UNIV ?S xi";  
   proof (rule reals_complete);
   
     txt {* The set $S$ is non-empty, since $a\ap\zero \in S$: *};
 
-    from vs; have "a 0 \\<in> ?S"; by force;
-    thus "\\<exists>X. X \\<in> ?S"; ..;
+    from vs; have "a 0 \<in> ?S"; by force;
+    thus "\<exists>X. X \<in> ?S"; ..;
 
     txt {* $b\ap \zero$ is an upper bound of $S$: *};
 
-    show "\\<exists>Y. isUb UNIV ?S Y"; 
+    show "\<exists>Y. isUb UNIV ?S Y"; 
     proof; 
       show "isUb UNIV ?S (b 0)";
       proof (intro isUbI setleI ballI);
-        show "b 0 \\<in> UNIV"; ..;
+        show "b 0 \<in> UNIV"; ..;
       next;
 
         txt {* Every element $y\in S$ is less than $b\ap \zero$: *};
 
-        fix y; assume y: "y \\<in> ?S"; 
-        from y; have "\\<exists>u \\<in> F. y = a u"; by fast;
+        fix y; assume y: "y \<in> ?S"; 
+        from y; have "\<exists>u \<in> F. y = a u"; by fast;
         thus "y <= b 0"; 
         proof;
-          fix u; assume "u \\<in> F"; 
+          fix u; assume "u \<in> F"; 
           assume "y = a u";
           also; have "a u <= b 0"; by (rule r) (simp!)+;
           finally; show ?thesis; .;
@@ -79,7 +79,7 @@
     qed;
   qed;
 
-  thus "\\<exists>xi. \\<forall>y \\<in> F. a y <= xi \\<and> xi <= b y"; 
+  thus "\<exists>xi. \<forall>y \<in> F. a y <= xi \<and> xi <= b y"; 
   proof (elim exE);
     fix xi; assume "isLub UNIV ?S xi"; 
     show ?thesis;
@@ -87,7 +87,7 @@
    
       txt {* For all $y\in F$ holds $a\ap y \leq \xi$: *};
      
-      fix y; assume y: "y \\<in> F";
+      fix y; assume y: "y \<in> F";
       show "a y <= xi";    
       proof (rule isUbD);  
         show "isUb UNIV ?S xi"; ..;
@@ -96,17 +96,17 @@
 
       txt {* For all $y\in F$ holds $\xi\leq b\ap y$: *};
 
-      fix y; assume "y \\<in> F";
+      fix y; assume "y \<in> F";
       show "xi <= b y";  
       proof (intro isLub_le_isUb isUbI setleI);
-        show "b y \\<in> UNIV"; ..;
-        show "\\<forall>ya \\<in> ?S. ya <= b y"; 
+        show "b y \<in> UNIV"; ..;
+        show "\<forall>ya \<in> ?S. ya <= b y"; 
         proof;
-          fix au; assume au: "au \\<in> ?S ";
-          hence "\\<exists>u \\<in> F. au = a u"; by fast;
+          fix au; assume au: "au \<in> ?S ";
+          hence "\<exists>u \<in> F. au = a u"; by fast;
           thus "au <= b y";
           proof;
-            fix u; assume "u \\<in> F"; assume "au = a u";  
+            fix u; assume "u \<in> F"; assume "au = a u";  
             also; have "... <= b y"; by (rule r);
             finally; show ?thesis; .;
           qed;
@@ -121,18 +121,18 @@
 is a linear extension of $h$ to $H'$. *};
 
 lemma h'_lf: 
-  "[| h' == (\\<lambda>x. let (y, a) = SOME (y, a). x = y + a \\<cdot> x0 \\<and> y \\<in> H 
+  "[| h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H 
                 in h y + a * xi);
-  H' == H + lin x0; is_subspace H E; is_linearform H h; x0 \\<notin> H; 
-  x0 \\<in> E; x0 \\<noteq> 0; is_vectorspace E |]
+  H' == H + lin x0; is_subspace H E; is_linearform H h; x0 \<notin> H; 
+  x0 \<in> E; x0 \<noteq> 0; is_vectorspace E |]
   ==> is_linearform H' h'";
 proof -;
   assume h'_def: 
-    "h' == (\\<lambda>x. let (y, a) = SOME (y, a). x = y + a \\<cdot> x0 \\<and> y \\<in> H 
+    "h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H 
                in h y + a * xi)"
     and H'_def: "H' == H + lin x0" 
-    and vs: "is_subspace H E" "is_linearform H h" "x0 \\<notin> H"
-      "x0 \\<noteq> 0" "x0 \\<in> E" "is_vectorspace E";
+    and vs: "is_subspace H E" "is_linearform H h" "x0 \<notin> H"
+      "x0 \<noteq> 0" "x0 \<in> E" "is_vectorspace E";
 
   have h': "is_vectorspace H'"; 
   proof (unfold H'_def, rule vs_sum_vs);
@@ -141,37 +141,37 @@
 
   show ?thesis;
   proof;
-    fix x1 x2; assume x1: "x1 \\<in> H'" and x2: "x2 \\<in> H'"; 
+    fix x1 x2; assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'"; 
 
     txt{* We now have to show that $h'$ is additive, i.~e.\
     $h' \ap (x_1\plus x_2) = h'\ap x_1 + h'\ap x_2$
     for $x_1, x_2\in H$. *}; 
 
-    have x1x2: "x1 + x2 \\<in> H'"; 
+    have x1x2: "x1 + x2 \<in> H'"; 
       by (rule vs_add_closed, rule h'); 
     from x1; 
-    have ex_x1: "\\<exists>y1 a1. x1 = y1 + a1 \\<cdot> x0  \\<and> y1 \\<in> H"; 
+    have ex_x1: "\<exists>y1 a1. x1 = y1 + a1 \<cdot> x0  \<and> y1 \<in> H"; 
       by (unfold H'_def vs_sum_def lin_def) fast;
     from x2; 
-    have ex_x2: "\\<exists>y2 a2. x2 = y2 + a2 \\<cdot> x0 \\<and> y2 \\<in> H"; 
+    have ex_x2: "\<exists>y2 a2. x2 = y2 + a2 \<cdot> x0 \<and> y2 \<in> H"; 
       by (unfold H'_def vs_sum_def lin_def) fast;
     from x1x2; 
-    have ex_x1x2: "\\<exists>y a. x1 + x2 = y + a \\<cdot> x0 \\<and> y \\<in> H";
+    have ex_x1x2: "\<exists>y a. x1 + x2 = y + a \<cdot> x0 \<and> y \<in> H";
       by (unfold H'_def vs_sum_def lin_def) fast;
 
     from ex_x1 ex_x2 ex_x1x2;
     show "h' (x1 + x2) = h' x1 + h' x2";
     proof (elim exE conjE);
       fix y1 y2 y a1 a2 a;
-      assume y1: "x1 = y1 + a1 \\<cdot> x0"     and y1': "y1 \\<in> H"
-         and y2: "x2 = y2 + a2 \\<cdot> x0"     and y2': "y2 \\<in> H" 
-         and y: "x1 + x2 = y + a \\<cdot> x0"   and y':  "y  \\<in> H"; 
+      assume y1: "x1 = y1 + a1 \<cdot> x0"     and y1': "y1 \<in> H"
+         and y2: "x2 = y2 + a2 \<cdot> x0"     and y2': "y2 \<in> H" 
+         and y: "x1 + x2 = y + a \<cdot> x0"   and y':  "y  \<in> H"; 
       txt {* \label{decomp-H-use}*}
-      have ya: "y1 + y2 = y \\<and> a1 + a2 = a"; 
+      have ya: "y1 + y2 = y \<and> a1 + a2 = a"; 
       proof (rule decomp_H')
-        show "y1 + y2 + (a1 + a2) \\<cdot> x0 = y + a \\<cdot> x0"; 
+        show "y1 + y2 + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0"; 
           by (simp! add: vs_add_mult_distrib2 [of E]);
-        show "y1 + y2 \\<in> H"; ..;
+        show "y1 + y2 \<in> H"; ..;
       qed;
 
       have "h' (x1 + x2) = h y + a * xi";
@@ -197,32 +197,32 @@
     *}; 
 
   next;  
-    fix c x1; assume x1: "x1 \\<in> H'";    
-    have ax1: "c \\<cdot> x1 \\<in> H'";
+    fix c x1; assume x1: "x1 \<in> H'";    
+    have ax1: "c \<cdot> x1 \<in> H'";
       by (rule vs_mult_closed, rule h');
     from x1; 
-    have ex_x: "!! x. x\\<in> H' ==> \\<exists>y a. x = y + a \\<cdot> x0 \\<and> y \\<in> H";
+    have ex_x: "!! x. x\<in> H' ==> \<exists>y a. x = y + a \<cdot> x0 \<and> y \<in> H";
       by (unfold H'_def vs_sum_def lin_def) fast;
 
-    from x1; have ex_x1: "\\<exists>y1 a1. x1 = y1 + a1 \\<cdot> x0 \\<and> y1 \\<in> H";
+    from x1; have ex_x1: "\<exists>y1 a1. x1 = y1 + a1 \<cdot> x0 \<and> y1 \<in> H";
       by (unfold H'_def vs_sum_def lin_def) fast;
-    with ex_x [of "c \\<cdot> x1", OF ax1];
-    show "h' (c \\<cdot> x1) = c * (h' x1)";  
+    with ex_x [of "c \<cdot> x1", OF ax1];
+    show "h' (c \<cdot> x1) = c * (h' x1)";  
     proof (elim exE conjE);
       fix y1 y a1 a; 
-      assume y1: "x1 = y1 + a1 \\<cdot> x0"     and y1': "y1 \\<in> H"
-        and y: "c \\<cdot> x1 = y  + a \\<cdot> x0"    and y': "y \\<in> H"; 
+      assume y1: "x1 = y1 + a1 \<cdot> x0"     and y1': "y1 \<in> H"
+        and y: "c \<cdot> x1 = y  + a \<cdot> x0"    and y': "y \<in> H"; 
 
-      have ya: "c \\<cdot> y1 = y \\<and> c * a1 = a"; 
+      have ya: "c \<cdot> y1 = y \<and> c * a1 = a"; 
       proof (rule decomp_H'); 
-	show "c \\<cdot> y1 + (c * a1) \\<cdot> x0 = y + a \\<cdot> x0"; 
+	show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0"; 
           by (simp! add: vs_add_mult_distrib1);
-        show "c \\<cdot> y1 \\<in> H"; ..;
+        show "c \<cdot> y1 \<in> H"; ..;
       qed;
 
-      have "h' (c \\<cdot> x1) = h y + a * xi"; 
+      have "h' (c \<cdot> x1) = h y + a * xi"; 
 	by (rule h'_definite);
-      also; have "... = h (c \\<cdot> y1) + (c * a1) * xi";
+      also; have "... = h (c \<cdot> y1) + (c * a1) * xi";
         by (simp add: ya);
       also; from vs y1'; have "... = c * h y1 + c * a1 * xi"; 
 	by (simp add: linearform_mult [of H]);
@@ -239,32 +239,32 @@
 is bounded by the seminorm $p$. *};
 
 lemma h'_norm_pres:
-  "[| h' == (\\<lambda>x. let (y, a) = SOME (y, a). x = y + a \\<cdot> x0 \\<and> y \\<in> H 
+  "[| h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H 
                  in h y + a * xi);
-  H' == H + lin x0; x0 \\<notin> H; x0 \\<in> E; x0 \\<noteq> 0; is_vectorspace E; 
+  H' == H + lin x0; x0 \<notin> H; x0 \<in> E; x0 \<noteq> 0; is_vectorspace E; 
   is_subspace H E; is_seminorm E p; is_linearform H h; 
-  \\<forall>y \\<in> H. h y <= p y; 
-  \\<forall>y \\<in> H. - p (y + x0) - h y <= xi \\<and> xi <= p (y + x0) - h y |]
-   ==> \\<forall>x \\<in> H'. h' x <= p x"; 
+  \<forall>y \<in> H. h y <= p y; 
+  \<forall>y \<in> H. - p (y + x0) - h y <= xi \<and> xi <= p (y + x0) - h y |]
+   ==> \<forall>x \<in> H'. h' x <= p x"; 
 proof; 
   assume h'_def: 
-    "h' == (\\<lambda>x. let (y, a) = SOME (y, a). x = y + a \\<cdot> x0 \\<and> y \\<in> H 
+    "h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H 
                in (h y) + a * xi)"
     and H'_def: "H' == H + lin x0" 
-    and vs: "x0 \\<notin> H" "x0 \\<in> E" "x0 \\<noteq> 0" "is_vectorspace E" 
+    and vs: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0" "is_vectorspace E" 
             "is_subspace H E" "is_seminorm E p" "is_linearform H h" 
-    and a: "\\<forall>y \\<in> H. h y <= p y";
-  presume a1: "\\<forall>ya \\<in> H. - p (ya + x0) - h ya <= xi";
-  presume a2: "\\<forall>ya \\<in> H. xi <= p (ya + x0) - h ya";
-  fix x; assume "x \\<in> H'"; 
+    and a: "\<forall>y \<in> H. h y <= p y";
+  presume a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya <= xi";
+  presume a2: "\<forall>ya \<in> H. xi <= p (ya + x0) - h ya";
+  fix x; assume "x \<in> H'"; 
   have ex_x: 
-    "!! x. x \\<in> H' ==> \\<exists>y a. x = y + a \\<cdot> x0 \\<and> y \\<in> H";
+    "!! x. x \<in> H' ==> \<exists>y a. x = y + a \<cdot> x0 \<and> y \<in> H";
     by (unfold H'_def vs_sum_def lin_def) fast;
-  have "\\<exists>y a. x = y + a \\<cdot> x0 \\<and> y \\<in> H";
+  have "\<exists>y a. x = y + a \<cdot> x0 \<and> y \<in> H";
     by (rule ex_x);
   thus "h' x <= p x";
   proof (elim exE conjE);
-    fix y a; assume x: "x = y + a \\<cdot> x0" and y: "y \\<in> H";
+    fix y a; assume x: "x = y + a \<cdot> x0" and y: "y \<in> H";
     have "h' x = h y + a * xi";
       by (rule h'_definite);
 
@@ -272,7 +272,7 @@
     $h\ap y + a \cdot \xi\leq  p\ap (y\plus a \mult x_0)$ 
     by case analysis on $a$. *};
 
-    also; have "... <= p (y + a \\<cdot> x0)";
+    also; have "... <= p (y + a \<cdot> x0)";
     proof (rule linorder_less_split); 
 
       assume z: "a = #0"; 
@@ -282,28 +282,28 @@
     taken as $y/a$: *};
 
     next;
-      assume lz: "a < #0"; hence nz: "a \\<noteq> #0"; by simp;
+      assume lz: "a < #0"; hence nz: "a \<noteq> #0"; by simp;
       from a1; 
-      have "- p (rinv a \\<cdot> y + x0) - h (rinv a \\<cdot> y) <= xi";
+      have "- p (rinv a \<cdot> y + x0) - h (rinv a \<cdot> y) <= xi";
         by (rule bspec) (simp!);
 
       txt {* The thesis for this case now follows by a short  
       calculation. *};      
-      hence "a * xi <= a * (- p (rinv a \\<cdot> y + x0) - h (rinv a \\<cdot> y))";
+      hence "a * xi <= a * (- p (rinv a \<cdot> y + x0) - h (rinv a \<cdot> y))";
         by (rule real_mult_less_le_anti [OF lz]);
       also; 
-      have "... = - a * (p (rinv a \\<cdot> y + x0)) - a * (h (rinv a \\<cdot> y))";
+      have "... = - a * (p (rinv a \<cdot> y + x0)) - a * (h (rinv a \<cdot> y))";
         by (rule real_mult_diff_distrib);
       also; from lz vs y; 
-      have "- a * (p (rinv a \\<cdot> y + x0)) = p (a \\<cdot> (rinv a \\<cdot> y + x0))";
+      have "- a * (p (rinv a \<cdot> y + x0)) = p (a \<cdot> (rinv a \<cdot> y + x0))";
         by (simp add: seminorm_abs_homogenous abs_minus_eqI2);
-      also; from nz vs y; have "... = p (y + a \\<cdot> x0)";
+      also; from nz vs y; have "... = p (y + a \<cdot> x0)";
         by (simp add: vs_add_mult_distrib1);
-      also; from nz vs y; have "a * (h (rinv a \\<cdot> y)) =  h y";
+      also; from nz vs y; have "a * (h (rinv a \<cdot> y)) =  h y";
         by (simp add: linearform_mult [RS sym]);
-      finally; have "a * xi <= p (y + a \\<cdot> x0) - h y"; .;
+      finally; have "a * xi <= p (y + a \<cdot> x0) - h y"; .;
 
-      hence "h y + a * xi <= h y + p (y + a \\<cdot> x0) - h y";
+      hence "h y + a * xi <= h y + p (y + a \<cdot> x0) - h y";
         by (simp add: real_add_left_cancel_le);
       thus ?thesis; by simp;
 
@@ -311,28 +311,28 @@
       taken as $y/a$: *};
 
     next; 
-      assume gz: "#0 < a"; hence nz: "a \\<noteq> #0"; by simp;
-      from a2; have "xi <= p (rinv a \\<cdot> y + x0) - h (rinv a \\<cdot> y)";
+      assume gz: "#0 < a"; hence nz: "a \<noteq> #0"; by simp;
+      from a2; have "xi <= p (rinv a \<cdot> y + x0) - h (rinv a \<cdot> y)";
         by (rule bspec) (simp!);
 
       txt {* The thesis for this case follows by a short
       calculation: *};
 
       with gz; 
-      have "a * xi <= a * (p (rinv a \\<cdot> y + x0) - h (rinv a \\<cdot> y))";
+      have "a * xi <= a * (p (rinv a \<cdot> y + x0) - h (rinv a \<cdot> y))";
         by (rule real_mult_less_le_mono);
-      also; have "... = a * p (rinv a \\<cdot> y + x0) - a * h (rinv a \\<cdot> y)";
+      also; have "... = a * p (rinv a \<cdot> y + x0) - a * h (rinv a \<cdot> y)";
         by (rule real_mult_diff_distrib2); 
       also; from gz vs y; 
-      have "a * p (rinv a \\<cdot> y + x0) = p (a \\<cdot> (rinv a \\<cdot> y + x0))";
+      have "a * p (rinv a \<cdot> y + x0) = p (a \<cdot> (rinv a \<cdot> y + x0))";
         by (simp add: seminorm_abs_homogenous abs_eqI2);
-      also; from nz vs y; have "... = p (y + a \\<cdot> x0)";
+      also; from nz vs y; have "... = p (y + a \<cdot> x0)";
         by (simp add: vs_add_mult_distrib1);
-      also; from nz vs y; have "a * h (rinv a \\<cdot> y) = h y";
+      also; from nz vs y; have "a * h (rinv a \<cdot> y) = h y";
         by (simp add: linearform_mult [RS sym]); 
-      finally; have "a * xi <= p (y + a \\<cdot> x0) - h y"; .;
+      finally; have "a * xi <= p (y + a \<cdot> x0) - h y"; .;
  
-      hence "h y + a * xi <= h y + (p (y + a \\<cdot> x0) - h y)";
+      hence "h y + a * xi <= h y + (p (y + a \<cdot> x0) - h y)";
         by (simp add: real_add_left_cancel_le);
       thus ?thesis; by simp;
     qed;
diff -r 50ec59aff389 -r 3324cbbecef8 src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Wed Aug 02 19:40:14 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Thu Aug 03 00:34:22 2000 +0200
@@ -24,43 +24,43 @@
 one of the elements of the chain. *}
 
 lemma some_H'h't:
-  "[| M = norm_pres_extensions E p F f; c \\<in> chain M; 
-  graph H h = \\<Union>c; x \\<in> H |]
-   ==> \\<exists>H' h'. graph H' h' \\<in> c \\<and> (x, h x) \\<in> graph H' h' 
-       \\<and> is_linearform H' h' \\<and> is_subspace H' E 
-       \\<and> is_subspace F H' \\<and> graph F f \\<subseteq> graph H' h' 
-       \\<and> (\\<forall>x \\<in> H'. h' x <= p x)"
+  "[| M = norm_pres_extensions E p F f; c \<in> chain M; 
+  graph H h = \<Union>c; x \<in> H |]
+   ==> \<exists>H' h'. graph H' h' \<in> c \<and> (x, h x) \<in> graph H' h' 
+       \<and> is_linearform H' h' \<and> is_subspace H' E 
+       \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' 
+       \<and> (\<forall>x \<in> H'. h' x <= p x)"
 proof -
-  assume m: "M = norm_pres_extensions E p F f" and "c \\<in> chain M"
-     and u: "graph H h = \\<Union>c" "x \\<in> H"
+  assume m: "M = norm_pres_extensions E p F f" and "c \<in> chain M"
+     and u: "graph H h = \<Union>c" "x \<in> H"
 
-  have h: "(x, h x) \\<in> graph H h" ..
-  with u have "(x, h x) \\<in> \\<Union>c" by simp
-  hence ex1: "\\<exists>g \\<in> c. (x, h x) \\<in> g" 
+  have h: "(x, h x) \<in> graph H h" ..
+  with u have "(x, h x) \<in> \<Union>c" by simp
+  hence ex1: "\<exists>g \<in> c. (x, h x) \<in> g" 
     by (simp only: Union_iff)
   thus ?thesis
   proof (elim bexE)
-    fix g assume g: "g \\<in> c" "(x, h x) \\<in> g"
-    have "c \\<subseteq> M" by (rule chainD2)
-    hence "g \\<in> M" ..
-    hence "g \\<in> norm_pres_extensions E p F f" by (simp only: m)
-    hence "\\<exists>H' h'. graph H' h' = g 
-                  \\<and> is_linearform H' h'
-                  \\<and> is_subspace H' E
-                  \\<and> is_subspace F H'
-                  \\<and> graph F f \\<subseteq> graph H' h'
-                  \\<and> (\\<forall>x \\<in> H'. h' x <= p x)"
+    fix g assume g: "g \<in> c" "(x, h x) \<in> g"
+    have "c \<subseteq> M" by (rule chainD2)
+    hence "g \<in> M" ..
+    hence "g \<in> norm_pres_extensions E p F f" by (simp only: m)
+    hence "\<exists>H' h'. graph H' h' = g 
+                  \<and> is_linearform H' h'
+                  \<and> is_subspace H' E
+                  \<and> is_subspace F H'
+                  \<and> graph F f \<subseteq> graph H' h'
+                  \<and> (\<forall>x \<in> H'. h' x <= p x)"
       by (rule norm_pres_extension_D)
     thus ?thesis
     proof (elim exE conjE) 
       fix H' h' 
       assume "graph H' h' = g" "is_linearform H' h'" 
         "is_subspace H' E" "is_subspace F H'" 
-        "graph F f \\<subseteq> graph H' h'" "\\<forall>x \\<in> H'. h' x <= p x"
+        "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x <= p x"
       show ?thesis 
       proof (intro exI conjI)
-        show "graph H' h' \\<in> c" by (simp!)
-        show "(x, h x) \\<in> graph H' h'" by (simp!)
+        show "graph H' h' \<in> c" by (simp!)
+        show "(x, h x) \<in> graph H' h'" by (simp!)
       qed
     qed
   qed
@@ -74,29 +74,29 @@
 *}
 
 lemma some_H'h': 
-  "[| M = norm_pres_extensions E p F f; c \\<in> chain M; 
-  graph H h = \\<Union>c; x \\<in> H |] 
-  ==> \\<exists>H' h'. x \\<in> H' \\<and> graph H' h' \\<subseteq> graph H h 
-      \\<and> is_linearform H' h' \\<and> is_subspace H' E \\<and> is_subspace F H'
-      \\<and> graph F f \\<subseteq> graph H' h' \\<and> (\\<forall>x \\<in> H'. h' x <= p x)" 
+  "[| M = norm_pres_extensions E p F f; c \<in> chain M; 
+  graph H h = \<Union>c; x \<in> H |] 
+  ==> \<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h 
+      \<and> is_linearform H' h' \<and> is_subspace H' E \<and> is_subspace F H'
+      \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x <= p x)" 
 proof -
-  assume "M = norm_pres_extensions E p F f" and cM: "c \\<in> chain M"
-     and u: "graph H h = \\<Union>c" "x \\<in> H"  
+  assume "M = norm_pres_extensions E p F f" and cM: "c \<in> chain M"
+     and u: "graph H h = \<Union>c" "x \<in> H"  
 
-  have "\\<exists>H' h'. graph H' h' \\<in> c \\<and> (x, h x) \\<in> graph H' h' 
-       \\<and> is_linearform H' h' \\<and> is_subspace H' E 
-       \\<and> is_subspace F H' \\<and> graph F f \\<subseteq> graph H' h' 
-       \\<and> (\\<forall>x \\<in> H'. h' x <= p x)"
+  have "\<exists>H' h'. graph H' h' \<in> c \<and> (x, h x) \<in> graph H' h' 
+       \<and> is_linearform H' h' \<and> is_subspace H' E 
+       \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' 
+       \<and> (\<forall>x \<in> H'. h' x <= p x)"
     by (rule some_H'h't)
   thus ?thesis 
   proof (elim exE conjE)
-    fix H' h' assume "(x, h x) \\<in> graph H' h'" "graph H' h' \\<in> c"
+    fix H' h' assume "(x, h x) \<in> graph H' h'" "graph H' h' \<in> c"
       "is_linearform H' h'" "is_subspace H' E" "is_subspace F H'" 
-      "graph F f \\<subseteq> graph H' h'" "\\<forall>x \\<in> H'. h' x <= p x"
+      "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x <= p x"
     show ?thesis
     proof (intro exI conjI)
-      show "x \\<in> H'" by (rule graphD1)
-      from cM u show "graph H' h' \\<subseteq> graph H h" 
+      show "x \<in> H'" by (rule graphD1)
+      from cM u show "graph H' h' \<subseteq> graph H h" 
         by (simp! only: chain_ball_Union_upper)
     qed
   qed
@@ -108,48 +108,48 @@
 $h'$, such that $h$ extends $h'$. *}
 
 lemma some_H'h'2: 
-  "[| M = norm_pres_extensions E p F f; c \\<in> chain M; 
-  graph H h = \\<Union>c;  x \\<in> H; y \\<in> H |] 
-  ==> \\<exists>H' h'. x \\<in> H' \\<and> y \\<in> H' \\<and> graph H' h' \\<subseteq> graph H h 
-      \\<and> is_linearform H' h' \\<and> is_subspace H' E \\<and> is_subspace F H'
-      \\<and> graph F f \\<subseteq> graph H' h' \\<and> (\\<forall>x \\<in> H'. h' x <= p x)" 
+  "[| M = norm_pres_extensions E p F f; c \<in> chain M; 
+  graph H h = \<Union>c;  x \<in> H; y \<in> H |] 
+  ==> \<exists>H' h'. x \<in> H' \<and> y \<in> H' \<and> graph H' h' \<subseteq> graph H h 
+      \<and> is_linearform H' h' \<and> is_subspace H' E \<and> is_subspace F H'
+      \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x <= p x)" 
 proof -
-  assume "M = norm_pres_extensions E p F f" "c \\<in> chain M" 
-         "graph H h = \\<Union>c" "x \\<in> H" "y \\<in> H"
+  assume "M = norm_pres_extensions E p F f" "c \<in> chain M" 
+         "graph H h = \<Union>c" "x \<in> H" "y \<in> H"
 
   txt {* $x$ is in the domain $H'$ of some function $h'$, 
   such that $h$ extends $h'$. *} 
 
-  have e1: "\\<exists>H' h'. graph H' h' \\<in> c \\<and> (x, h x) \\<in> graph H' h'
-       \\<and> is_linearform H' h' \\<and> is_subspace H' E 
-       \\<and> is_subspace F H' \\<and> graph F f \\<subseteq> graph H' h' 
-       \\<and> (\\<forall>x \\<in> H'. h' x <= p x)"
+  have e1: "\<exists>H' h'. graph H' h' \<in> c \<and> (x, h x) \<in> graph H' h'
+       \<and> is_linearform H' h' \<and> is_subspace H' E 
+       \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' 
+       \<and> (\<forall>x \<in> H'. h' x <= p x)"
     by (rule some_H'h't)
 
   txt {* $y$ is in the domain $H''$ of some function $h''$,
   such that $h$ extends $h''$. *} 
 
-  have e2: "\\<exists>H'' h''. graph H'' h'' \\<in> c \\<and> (y, h y) \\<in> graph H'' h''
-       \\<and> is_linearform H'' h'' \\<and> is_subspace H'' E 
-       \\<and> is_subspace F H'' \\<and> graph F f \\<subseteq> graph H'' h'' 
-       \\<and> (\\<forall>x \\<in> H''. h'' x <= p x)"
+  have e2: "\<exists>H'' h''. graph H'' h'' \<in> c \<and> (y, h y) \<in> graph H'' h''
+       \<and> is_linearform H'' h'' \<and> is_subspace H'' E 
+       \<and> is_subspace F H'' \<and> graph F f \<subseteq> graph H'' h'' 
+       \<and> (\<forall>x \<in> H''. h'' x <= p x)"
     by (rule some_H'h't)
 
   from e1 e2 show ?thesis 
   proof (elim exE conjE)
-    fix H' h' assume "(y, h y) \\<in> graph H' h'" "graph H' h' \\<in> c"
+    fix H' h' assume "(y, h y) \<in> graph H' h'" "graph H' h' \<in> c"
       "is_linearform H' h'" "is_subspace H' E" "is_subspace F H'" 
-      "graph F f \\<subseteq> graph H' h'" "\\<forall>x \\<in> H'. h' x <= p x"
+      "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x <= p x"
 
-    fix H'' h'' assume "(x, h x) \\<in> graph H'' h''" "graph H'' h'' \\<in> c"
+    fix H'' h'' assume "(x, h x) \<in> graph H'' h''" "graph H'' h'' \<in> c"
       "is_linearform H'' h''" "is_subspace H'' E" "is_subspace F H''"
-      "graph F f \\<subseteq> graph H'' h''" "\\<forall>x \\<in> H''. h'' x <= p x"
+      "graph F f \<subseteq> graph H'' h''" "\<forall>x \<in> H''. h'' x <= p x"
 
    txt {* Since both $h'$ and $h''$ are elements of the chain,  
    $h''$ is an extension of $h'$ or vice versa. Thus both 
    $x$ and $y$ are contained in the greater one. \label{cases1}*}
 
-    have "graph H'' h'' \\<subseteq> graph H' h' | graph H' h' \\<subseteq> graph H'' h''"
+    have "graph H'' h'' \<subseteq> graph H' h' | graph H' h' \<subseteq> graph H'' h''"
       (is "?case1 | ?case2")
       by (rule chainD)
     thus ?thesis
@@ -157,24 +157,24 @@
       assume ?case1
       show ?thesis
       proof (intro exI conjI)
-        have "(x, h x) \\<in> graph H'' h''" .
-        also have "... \\<subseteq> graph H' h'" .
-        finally have xh:"(x, h x) \\<in> graph H' h'" .
-        thus x: "x \\<in> H'" ..
-        show y: "y \\<in> H'" ..
-        show "graph H' h' \\<subseteq> graph H h"
+        have "(x, h x) \<in> graph H'' h''" .
+        also have "... \<subseteq> graph H' h'" .
+        finally have xh:"(x, h x) \<in> graph H' h'" .
+        thus x: "x \<in> H'" ..
+        show y: "y \<in> H'" ..
+        show "graph H' h' \<subseteq> graph H h"
           by (simp! only: chain_ball_Union_upper)
       qed
     next
       assume ?case2
       show ?thesis
       proof (intro exI conjI)
-        show x: "x \\<in> H''" ..
-        have "(y, h y) \\<in> graph H' h'" by (simp!)
-        also have "... \\<subseteq> graph H'' h''" .
-        finally have yh: "(y, h y) \\<in> graph H'' h''" .
-        thus y: "y \\<in> H''" ..
-        show "graph H'' h'' \\<subseteq> graph H h"
+        show x: "x \<in> H''" ..
+        have "(y, h y) \<in> graph H' h'" by (simp!)
+        also have "... \<subseteq> graph H'' h''" .
+        finally have yh: "(y, h y) \<in> graph H'' h''" .
+        thus y: "y \<in> H''" ..
+        show "graph H'' h'' \<subseteq> graph H h"
           by (simp! only: chain_ball_Union_upper)
       qed
     qed
@@ -187,11 +187,11 @@
 of a chain $c$ is definite, i.~e.~t is the graph of a function. *}
 
 lemma sup_definite: 
-  "[| M == norm_pres_extensions E p F f; c \\<in> chain M; 
-  (x, y) \\<in> \\<Union>c; (x, z) \\<in> \\<Union>c |] ==> z = y"
+  "[| M == norm_pres_extensions E p F f; c \<in> chain M; 
+  (x, y) \<in> \<Union>c; (x, z) \<in> \<Union>c |] ==> z = y"
 proof - 
-  assume "c \\<in> chain M" "M == norm_pres_extensions E p F f"
-    "(x, y) \\<in> \\<Union>c" "(x, z) \\<in> \\<Union>c"
+  assume "c \<in> chain M" "M == norm_pres_extensions E p F f"
+    "(x, y) \<in> \<Union>c" "(x, z) \<in> \<Union>c"
   thus ?thesis
   proof (elim UnionE chainE2)
 
@@ -200,13 +200,13 @@
     both $G_1$ and $G_2$ are members of $c$.*}
 
     fix G1 G2 assume
-      "(x, y) \\<in> G1" "G1 \\<in> c" "(x, z) \\<in> G2" "G2 \\<in> c" "c \\<subseteq> M"
+      "(x, y) \<in> G1" "G1 \<in> c" "(x, z) \<in> G2" "G2 \<in> c" "c \<subseteq> M"
 
-    have "G1 \\<in> M" ..
-    hence e1: "\\<exists>H1 h1. graph H1 h1 = G1"  
+    have "G1 \<in> M" ..
+    hence e1: "\<exists>H1 h1. graph H1 h1 = G1"  
       by (force! dest: norm_pres_extension_D)
-    have "G2 \\<in> M" ..
-    hence e2: "\\<exists>H2 h2. graph H2 h2 = G2"  
+    have "G2 \<in> M" ..
+    hence e2: "\<exists>H2 h2. graph H2 h2 = G2"  
       by (force! dest: norm_pres_extension_D)
     from e1 e2 show ?thesis 
     proof (elim exE)
@@ -216,20 +216,20 @@
       txt{* $G_1$ is contained in $G_2$ or vice versa, 
       since both $G_1$ and $G_2$ are members of $c$. \label{cases2}*}
 
-      have "G1 \\<subseteq> G2 | G2 \\<subseteq> G1" (is "?case1 | ?case2") ..
+      have "G1 \<subseteq> G2 | G2 \<subseteq> G1" (is "?case1 | ?case2") ..
       thus ?thesis
       proof
         assume ?case1
-        have "(x, y) \\<in> graph H2 h2" by (force!)
+        have "(x, y) \<in> graph H2 h2" by (force!)
         hence "y = h2 x" ..
-        also have "(x, z) \\<in> graph H2 h2" by (simp!)
+        also have "(x, z) \<in> graph H2 h2" by (simp!)
         hence "z = h2 x" ..
         finally show ?thesis .
       next
         assume ?case2
-        have "(x, y) \\<in> graph H1 h1" by (simp!)
+        have "(x, y) \<in> graph H1 h1" by (simp!)
         hence "y = h1 x" ..
-        also have "(x, z) \\<in> graph H1 h1" by (force!)
+        also have "(x, z) \<in> graph H1 h1" by (force!)
         hence "z = h1 x" ..
         finally show ?thesis .
       qed
@@ -244,56 +244,56 @@
 function $h'$ is linear by construction of $M$.  *}
 
 lemma sup_lf: 
-  "[| M = norm_pres_extensions E p F f; c \\<in> chain M; 
-  graph H h = \\<Union>c |] ==> is_linearform H h"
+  "[| M = norm_pres_extensions E p F f; c \<in> chain M; 
+  graph H h = \<Union>c |] ==> is_linearform H h"
 proof - 
-  assume "M = norm_pres_extensions E p F f" "c \\<in> chain M"
-         "graph H h = \\<Union>c"
+  assume "M = norm_pres_extensions E p F f" "c \<in> chain M"
+         "graph H h = \<Union>c"
  
   show "is_linearform H h"
   proof
-    fix x y assume "x \\<in> H" "y \\<in> H" 
-    have "\\<exists>H' h'. x \\<in> H' \\<and> y \\<in> H' \\<and> graph H' h' \\<subseteq> graph H h 
-            \\<and> is_linearform H' h' \\<and> is_subspace H' E 
-            \\<and> is_subspace F H' \\<and> graph F f \\<subseteq> graph H' h'
-            \\<and> (\\<forall>x \\<in> H'. h' x <= p x)"
+    fix x y assume "x \<in> H" "y \<in> H" 
+    have "\<exists>H' h'. x \<in> H' \<and> y \<in> H' \<and> graph H' h' \<subseteq> graph H h 
+            \<and> is_linearform H' h' \<and> is_subspace H' E 
+            \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
+            \<and> (\<forall>x \<in> H'. h' x <= p x)"
       by (rule some_H'h'2)
 
     txt {* We have to show that $h$ is additive. *}
 
     thus "h (x + y) = h x + h y" 
     proof (elim exE conjE)
-      fix H' h' assume "x \\<in> H'" "y \\<in> H'" 
-        and b: "graph H' h' \\<subseteq> graph H h" 
+      fix H' h' assume "x \<in> H'" "y \<in> H'" 
+        and b: "graph H' h' \<subseteq> graph H h" 
         and "is_linearform H' h'" "is_subspace H' E"
       have "h' (x + y) = h' x + h' y" 
         by (rule linearform_add)
       also have "h' x = h x" ..
       also have "h' y = h y" ..
-      also have "x + y \\<in> H'" ..
+      also have "x + y \<in> H'" ..
       with b have "h' (x + y) = h (x + y)" ..
       finally show ?thesis .
     qed
   next  
-    fix a x assume "x \\<in> H"
-    have "\\<exists>H' h'. x \\<in> H' \\<and> graph H' h' \\<subseteq> graph H h 
-            \\<and> is_linearform H' h' \\<and> is_subspace H' E
-            \\<and> is_subspace F H' \\<and> graph F f \\<subseteq> graph H' h' 
-            \\<and> (\\<forall>x \\<in> H'. h' x <= p x)"
+    fix a x assume "x \<in> H"
+    have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h 
+            \<and> is_linearform H' h' \<and> is_subspace H' E
+            \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' 
+            \<and> (\<forall>x \<in> H'. h' x <= p x)"
       by (rule some_H'h')
 
     txt{* We have to show that $h$ is multiplicative. *}
 
-    thus "h (a \\<cdot> x) = a * h x"
+    thus "h (a \<cdot> x) = a * h x"
     proof (elim exE conjE)
-      fix H' h' assume "x \\<in> H'"
-        and b: "graph H' h' \\<subseteq> graph H h" 
+      fix H' h' assume "x \<in> H'"
+        and b: "graph H' h' \<subseteq> graph H h" 
         and "is_linearform H' h'" "is_subspace H' E"
-      have "h' (a \\<cdot> x) = a * h' x" 
+      have "h' (a \<cdot> x) = a * h' x" 
         by (rule linearform_mult)
       also have "h' x = h x" ..
-      also have "a \\<cdot> x \\<in> H'" ..
-      with b have "h' (a \\<cdot> x) = h (a \\<cdot> x)" ..
+      also have "a \<cdot> x \<in> H'" ..
+      with b have "h' (a \<cdot> x) = h (a \<cdot> x)" ..
       finally show ?thesis .
     qed
   qed
@@ -306,34 +306,34 @@
 for every element of the chain.*}
 
 lemma sup_ext:
-  "[| graph H h = \\<Union>c; M = norm_pres_extensions E p F f; 
-  c \\<in> chain M; \\<exists>x. x \\<in> c |] ==> graph F f \\<subseteq> graph H h"
+  "[| graph H h = \<Union>c; M = norm_pres_extensions E p F f; 
+  c \<in> chain M; \<exists>x. x \<in> c |] ==> graph F f \<subseteq> graph H h"
 proof -
-  assume "M = norm_pres_extensions E p F f" "c \\<in> chain M" 
-         "graph H h = \\<Union>c"
-  assume "\\<exists>x. x \\<in> c"
+  assume "M = norm_pres_extensions E p F f" "c \<in> chain M" 
+         "graph H h = \<Union>c"
+  assume "\<exists>x. x \<in> c"
   thus ?thesis 
   proof
-    fix x assume "x \\<in> c" 
-    have "c \\<subseteq> M" by (rule chainD2)
-    hence "x \\<in> M" ..
-    hence "x \\<in> norm_pres_extensions E p F f" by (simp!)
+    fix x assume "x \<in> c" 
+    have "c \<subseteq> M" by (rule chainD2)
+    hence "x \<in> M" ..
+    hence "x \<in> norm_pres_extensions E p F f" by (simp!)
 
-    hence "\\<exists>G g. graph G g = x
-             \\<and> is_linearform G g 
-             \\<and> is_subspace G E
-             \\<and> is_subspace F G
-             \\<and> graph F f \\<subseteq> graph G g 
-             \\<and> (\\<forall>x \\<in> G. g x <= p x)"
+    hence "\<exists>G g. graph G g = x
+             \<and> is_linearform G g 
+             \<and> is_subspace G E
+             \<and> is_subspace F G
+             \<and> graph F f \<subseteq> graph G g 
+             \<and> (\<forall>x \<in> G. g x <= p x)"
       by (simp! add: norm_pres_extension_D)
 
     thus ?thesis 
     proof (elim exE conjE) 
-      fix G g assume "graph F f \\<subseteq> graph G g"
+      fix G g assume "graph F f \<subseteq> graph G g"
       also assume "graph G g = x"
-      also have "... \\<in> c" .
-      hence "x \\<subseteq> \\<Union>c" by fast
-      also have [RS sym]: "graph H h = \\<Union>c" .
+      also have "... \<in> c" .
+      hence "x \<subseteq> \<Union>c" by fast
+      also have [RS sym]: "graph H h = \<Union>c" .
       finally show ?thesis .
     qed
   qed
@@ -345,30 +345,30 @@
 vector space. *}
 
 lemma sup_supF: 
-  "[|  graph H h = \\<Union>c; M = norm_pres_extensions E p F f; 
-  c \\<in> chain M; \\<exists>x. x \\<in> c; is_subspace F E; is_vectorspace E |] 
+  "[|  graph H h = \<Union>c; M = norm_pres_extensions E p F f; 
+  c \<in> chain M; \<exists>x. x \<in> c; is_subspace F E; is_vectorspace E |] 
   ==> is_subspace F H"
 proof - 
-  assume "M = norm_pres_extensions E p F f" "c \\<in> chain M" "\\<exists>x. x \\<in> c"
-    "graph H h = \\<Union>c" "is_subspace F E" "is_vectorspace E"
+  assume "M = norm_pres_extensions E p F f" "c \<in> chain M" "\<exists>x. x \<in> c"
+    "graph H h = \<Union>c" "is_subspace F E" "is_vectorspace E"
 
   show ?thesis 
   proof
-    show "0 \\<in> F" ..
-    show "F \\<subseteq> H" 
+    show "0 \<in> F" ..
+    show "F \<subseteq> H" 
     proof (rule graph_extD2)
-      show "graph F f \\<subseteq> graph H h"
+      show "graph F f \<subseteq> graph H h"
         by (rule sup_ext)
     qed
-    show "\\<forall>x \\<in> F. \\<forall>y \\<in> F. x + y \\<in> F" 
+    show "\<forall>x \<in> F. \<forall>y \<in> F. x + y \<in> F" 
     proof (intro ballI) 
-      fix x y assume "x \\<in> F" "y \\<in> F"
-      show "x + y \\<in> F" by (simp!)
+      fix x y assume "x \<in> F" "y \<in> F"
+      show "x + y \<in> F" by (simp!)
     qed
-    show "\\<forall>x \\<in> F. \\<forall>a. a \\<cdot> x \\<in> F"
+    show "\<forall>x \<in> F. \<forall>a. a \<cdot> x \<in> F"
     proof (intro ballI allI)
-      fix x a assume "x\\<in>F"
-      show "a \\<cdot> x \\<in> F" by (simp!)
+      fix x a assume "x\<in>F"
+      show "a \<cdot> x \<in> F" by (simp!)
     qed
   qed
 qed
@@ -377,78 +377,78 @@
 of $E$. *}
 
 lemma sup_subE: 
-  "[| graph H h = \\<Union>c; M = norm_pres_extensions E p F f; 
-  c \\<in> chain M; \\<exists>x. x \\<in> c; is_subspace F E; is_vectorspace E |] 
+  "[| graph H h = \<Union>c; M = norm_pres_extensions E p F f; 
+  c \<in> chain M; \<exists>x. x \<in> c; is_subspace F E; is_vectorspace E |] 
   ==> is_subspace H E"
 proof - 
-  assume "M = norm_pres_extensions E p F f" "c \\<in> chain M" "\\<exists>x. x \\<in> c"
-    "graph H h = \\<Union>c" "is_subspace F E" "is_vectorspace E"
+  assume "M = norm_pres_extensions E p F f" "c \<in> chain M" "\<exists>x. x \<in> c"
+    "graph H h = \<Union>c" "is_subspace F E" "is_vectorspace E"
   show ?thesis 
   proof
  
     txt {* The $\zero$ element is in $H$, as $F$ is a subset 
     of $H$: *}
 
-    have "0 \\<in> F" ..
+    have "0 \<in> F" ..
     also have "is_subspace F H" by (rule sup_supF) 
-    hence "F \\<subseteq> H" ..
-    finally show "0 \\<in> H" .
+    hence "F \<subseteq> H" ..
+    finally show "0 \<in> H" .
 
     txt{* $H$ is a subset of $E$: *}
 
-    show "H \\<subseteq> E" 
+    show "H \<subseteq> E" 
     proof
-      fix x assume "x \\<in> H"
-      have "\\<exists>H' h'. x \\<in> H' \\<and> graph H' h' \\<subseteq> graph H h
-              \\<and> is_linearform H' h' \\<and> is_subspace H' E 
-              \\<and> is_subspace F H' \\<and> graph F f \\<subseteq> graph H' h' 
-              \\<and> (\\<forall>x \\<in> H'. h' x <= p x)" 
+      fix x assume "x \<in> H"
+      have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
+              \<and> is_linearform H' h' \<and> is_subspace H' E 
+              \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' 
+              \<and> (\<forall>x \<in> H'. h' x <= p x)" 
 	by (rule some_H'h')
-      thus "x \\<in> E" 
+      thus "x \<in> E" 
       proof (elim exE conjE)
-	fix H' h' assume "x \\<in> H'" "is_subspace H' E"
-        have "H' \\<subseteq> E" ..
-	thus "x \\<in> E" ..
+	fix H' h' assume "x \<in> H'" "is_subspace H' E"
+        have "H' \<subseteq> E" ..
+	thus "x \<in> E" ..
       qed
     qed
 
     txt{* $H$ is closed under addition: *}
 
-    show "\\<forall>x \\<in> H. \\<forall>y \\<in> H. x + y \\<in> H" 
+    show "\<forall>x \<in> H. \<forall>y \<in> H. x + y \<in> H" 
     proof (intro ballI) 
-      fix x y assume "x \\<in> H" "y \\<in> H"
-      have "\\<exists>H' h'. x \\<in> H' \\<and> y \\<in> H' \\<and> graph H' h' \\<subseteq> graph H h 
-              \\<and> is_linearform H' h' \\<and> is_subspace H' E 
-              \\<and> is_subspace F H' \\<and> graph F f \\<subseteq> graph H' h' 
-              \\<and> (\\<forall>x \\<in> H'. h' x <= p x)" 
+      fix x y assume "x \<in> H" "y \<in> H"
+      have "\<exists>H' h'. x \<in> H' \<and> y \<in> H' \<and> graph H' h' \<subseteq> graph H h 
+              \<and> is_linearform H' h' \<and> is_subspace H' E 
+              \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' 
+              \<and> (\<forall>x \<in> H'. h' x <= p x)" 
 	by (rule some_H'h'2) 
-      thus "x + y \\<in> H" 
+      thus "x + y \<in> H" 
       proof (elim exE conjE) 
 	fix H' h' 
-        assume "x \\<in> H'" "y \\<in> H'" "is_subspace H' E" 
-          "graph H' h' \\<subseteq> graph H h"
-        have "x + y \\<in> H'" ..
-	also have "H' \\<subseteq> H" ..
+        assume "x \<in> H'" "y \<in> H'" "is_subspace H' E" 
+          "graph H' h' \<subseteq> graph H h"
+        have "x + y \<in> H'" ..
+	also have "H' \<subseteq> H" ..
 	finally show ?thesis .
       qed
     qed      
 
     txt{* $H$ is closed under scalar multiplication: *}
 
-    show "\\<forall>x \\<in> H. \\<forall>a. a \\<cdot> x \\<in> H" 
+    show "\<forall>x \<in> H. \<forall>a. a \<cdot> x \<in> H" 
     proof (intro ballI allI) 
-      fix x a assume "x \\<in> H" 
-      have "\\<exists>H' h'. x \\<in> H' \\<and> graph H' h' \\<subseteq> graph H h
-              \\<and> is_linearform H' h' \\<and> is_subspace H' E 
-              \\<and> is_subspace F H' \\<and> graph F f \\<subseteq> graph H' h' 
-              \\<and> (\\<forall>x \\<in> H'. h' x <= p x)" 
+      fix x a assume "x \<in> H" 
+      have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
+              \<and> is_linearform H' h' \<and> is_subspace H' E 
+              \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' 
+              \<and> (\<forall>x \<in> H'. h' x <= p x)" 
 	by (rule some_H'h') 
-      thus "a \\<cdot> x \\<in> H" 
+      thus "a \<cdot> x \<in> H" 
       proof (elim exE conjE)
 	fix H' h' 
-        assume "x \\<in> H'" "is_subspace H' E" "graph H' h' \\<subseteq> graph H h"
-        have "a \\<cdot> x \\<in> H'" ..
-        also have "H' \\<subseteq> H" ..
+        assume "x \<in> H'" "is_subspace H' E" "graph H' h' \<subseteq> graph H h"
+        have "a \<cdot> x \<in> H'" ..
+        also have "H' \<subseteq> H" ..
 	finally show ?thesis .
       qed
     qed
@@ -461,21 +461,21 @@
 *}
 
 lemma sup_norm_pres:
-  "[| graph H h = \\<Union>c; M = norm_pres_extensions E p F f; 
-  c \\<in> chain M |] ==> \\<forall>x \\<in> H. h x <= p x"
+  "[| graph H h = \<Union>c; M = norm_pres_extensions E p F f; 
+  c \<in> chain M |] ==> \<forall>x \<in> H. h x <= p x"
 proof
-  assume "M = norm_pres_extensions E p F f" "c \\<in> chain M" 
-         "graph H h = \\<Union>c"
-  fix x assume "x \\<in> H"
-  have "\\<exists>H' h'. x \\<in> H' \\<and> graph H' h' \\<subseteq> graph H h 
-          \\<and> is_linearform H' h' \\<and> is_subspace H' E \\<and> is_subspace F H'
-          \\<and> graph F f \\<subseteq> graph H' h' \\<and> (\\<forall>x \\<in> H'. h' x <= p x)" 
+  assume "M = norm_pres_extensions E p F f" "c \<in> chain M" 
+         "graph H h = \<Union>c"
+  fix x assume "x \<in> H"
+  have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h 
+          \<and> is_linearform H' h' \<and> is_subspace H' E \<and> is_subspace F H'
+          \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x <= p x)" 
     by (rule some_H'h')
   thus "h x <= p x" 
   proof (elim exE conjE)
     fix H' h' 
-    assume "x \\<in> H'" "graph H' h' \\<subseteq> graph H h" 
-      and a: "\\<forall>x \\<in> H'. h' x <= p x"
+    assume "x \<in> H'" "graph H' h' \<subseteq> graph H h" 
+      and a: "\<forall>x \<in> H'. h' x <= p x"
     have [RS sym]: "h' x = h x" ..
     also from a have "h' x <= p x " ..
     finally show ?thesis .  
@@ -496,7 +496,7 @@
 lemma abs_ineq_iff: 
   "[| is_subspace H E; is_vectorspace E; is_seminorm E p; 
   is_linearform H h |] 
-  ==> (\\<forall>x \\<in> H. |h x| <= p x) = (\\<forall>x \\<in> H. h x <= p x)" 
+  ==> (\<forall>x \<in> H. |h x| <= p x) = (\<forall>x \<in> H. h x <= p x)" 
   (concl is "?L = ?R")
 proof -
   assume "is_subspace H E" "is_vectorspace E" "is_seminorm E p" 
@@ -507,7 +507,7 @@
     assume l: ?L
     show ?R
     proof
-      fix x assume x: "x \\<in> H"
+      fix x assume x: "x \<in> H"
       have "h x <= |h x|" by (rule abs_ge_self)
       also from l have "... <= p x" ..
       finally show "h x <= p x" .
@@ -516,7 +516,7 @@
     assume r: ?R
     show ?L
     proof 
-      fix x assume "x \\<in> H"
+      fix x assume "x \<in> H"
       show "!! a b :: real. [| - a <= b; b <= a |] ==> |b| <= a"
         by arith
       show "- p x <= h x"
@@ -526,7 +526,7 @@
 	also from r have "... <= p (- x)" by (simp!)
 	also have "... = p x" 
         proof (rule seminorm_minus)
-          show "x \\<in> E" ..
+          show "x \<in> E" ..
         qed
 	finally show "- h x <= p x" . 
       qed
diff -r 50ec59aff389 -r 3324cbbecef8 src/HOL/Real/HahnBanach/VectorSpace.thy
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Wed Aug 02 19:40:14 2000 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Thu Aug 03 00:34:22 2000 +0200
@@ -17,7 +17,7 @@
   prod  :: "[real, 'a::{plus, minus, zero}] => 'a"     (infixr "'(*')" 70)
 
 syntax (symbols)
-  prod  :: "[real, 'a] => 'a"                          (infixr "\\<cdot>" 70)
+  prod  :: "[real, 'a] => 'a"                          (infixr "\<cdot>" 70)
 
 
 subsection {* Vector space laws *}
@@ -34,42 +34,42 @@
 
 constdefs
   is_vectorspace :: "('a::{plus, minus, zero}) set => bool"
-  "is_vectorspace V == V \\<noteq> {}
-   \\<and> (\\<forall>x \\<in> V. \\<forall>y \\<in> V. \\<forall>z \\<in> V. \\<forall>a b.
-        x + y \\<in> V                                 
-      \\<and> a \\<cdot> x \\<in> V                                 
-      \\<and> (x + y) + z = x + (y + z)             
-      \\<and> x + y = y + x                           
-      \\<and> x - x = 0                               
-      \\<and> 0 + x = x                               
-      \\<and> a \\<cdot> (x + y) = a \\<cdot> x + a \\<cdot> y       
-      \\<and> (a + b) \\<cdot> x = a \\<cdot> x + b \\<cdot> x         
-      \\<and> (a * b) \\<cdot> x = a \\<cdot> b \\<cdot> x               
-      \\<and> #1 \\<cdot> x = x
-      \\<and> - x = (- #1) \\<cdot> x
-      \\<and> x - y = x + - y)"                             
+  "is_vectorspace V == V \<noteq> {}
+   \<and> (\<forall>x \<in> V. \<forall>y \<in> V. \<forall>z \<in> V. \<forall>a b.
+        x + y \<in> V                                 
+      \<and> a \<cdot> x \<in> V                                 
+      \<and> (x + y) + z = x + (y + z)             
+      \<and> x + y = y + x                           
+      \<and> x - x = 0                               
+      \<and> 0 + x = x                               
+      \<and> a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y       
+      \<and> (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x         
+      \<and> (a * b) \<cdot> x = a \<cdot> b \<cdot> x               
+      \<and> #1 \<cdot> x = x
+      \<and> - x = (- #1) \<cdot> x
+      \<and> x - y = x + - y)"                             
 
 text_raw {* \medskip *}
 text {* The corresponding introduction rule is:*}
 
 lemma vsI [intro]:
-  "[| 0 \\<in> V; 
-  \\<forall>x \\<in> V. \\<forall>y \\<in> V. x + y \\<in> V; 
-  \\<forall>x \\<in> V. \\<forall>a. a \\<cdot> x \\<in> V;  
-  \\<forall>x \\<in> V. \\<forall>y \\<in> V. \\<forall>z \\<in> V. (x + y) + z = x + (y + z);
-  \\<forall>x \\<in> V. \\<forall>y \\<in> V. x + y = y + x;
-  \\<forall>x \\<in> V. x - x = 0;
-  \\<forall>x \\<in> V. 0 + x = x;
-  \\<forall>x \\<in> V. \\<forall>y \\<in> V. \\<forall>a. a \\<cdot> (x + y) = a \\<cdot> x + a \\<cdot> y;
-  \\<forall>x \\<in> V. \\<forall>a b. (a + b) \\<cdot> x = a \\<cdot> x + b \\<cdot> x;
-  \\<forall>x \\<in> V. \\<forall>a b. (a * b) \\<cdot> x = a \\<cdot> b \\<cdot> x; 
-  \\<forall>x \\<in> V. #1 \\<cdot> x = x; 
-  \\<forall>x \\<in> V. - x = (- #1) \\<cdot> x; 
-  \\<forall>x \\<in> V. \\<forall>y \\<in> V. x - y = x + - y |] ==> is_vectorspace V"
+  "[| 0 \<in> V; 
+  \<forall>x \<in> V. \<forall>y \<in> V. x + y \<in> V; 
+  \<forall>x \<in> V. \<forall>a. a \<cdot> x \<in> V;  
+  \<forall>x \<in> V. \<forall>y \<in> V. \<forall>z \<in> V. (x + y) + z = x + (y + z);
+  \<forall>x \<in> V. \<forall>y \<in> V. x + y = y + x;
+  \<forall>x \<in> V. x - x = 0;
+  \<forall>x \<in> V. 0 + x = x;
+  \<forall>x \<in> V. \<forall>y \<in> V. \<forall>a. a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y;
+  \<forall>x \<in> V. \<forall>a b. (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x;
+  \<forall>x \<in> V. \<forall>a b. (a * b) \<cdot> x = a \<cdot> b \<cdot> x; 
+  \<forall>x \<in> V. #1 \<cdot> x = x; 
+  \<forall>x \<in> V. - x = (- #1) \<cdot> x; 
+  \<forall>x \<in> V. \<forall>y \<in> V. x - y = x + - y |] ==> is_vectorspace V"
 proof (unfold is_vectorspace_def, intro conjI ballI allI)
   fix x y z 
-  assume "x \\<in> V" "y \\<in> V" "z \\<in> V"
-    "\\<forall>x \\<in> V. \\<forall>y \\<in> V. \\<forall>z \\<in> V. x + y + z = x + (y + z)"
+  assume "x \<in> V" "y \<in> V" "z \<in> V"
+    "\<forall>x \<in> V. \<forall>y \<in> V. \<forall>z \<in> V. x + y + z = x + (y + z)"
   thus "x + y + z =  x + (y + z)" by blast
 qed force+
 
@@ -77,58 +77,58 @@
 text {* The corresponding destruction rules are: *}
 
 lemma negate_eq1: 
-  "[| is_vectorspace V; x \\<in> V |] ==> - x = (- #1) \\<cdot> x"
+  "[| is_vectorspace V; x \<in> V |] ==> - x = (- #1) \<cdot> x"
   by (unfold is_vectorspace_def) simp
 
 lemma diff_eq1: 
-  "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> x - y = x + - y"
+  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x - y = x + - y"
   by (unfold is_vectorspace_def) simp 
 
 lemma negate_eq2: 
-  "[| is_vectorspace V; x \\<in> V |] ==> (- #1) \\<cdot> x = - x"
+  "[| is_vectorspace V; x \<in> V |] ==> (- #1) \<cdot> x = - x"
   by (unfold is_vectorspace_def) simp
 
 lemma negate_eq2a: 
-  "[| is_vectorspace V; x \\<in> V |] ==> #-1 \\<cdot> x = - x"
+  "[| is_vectorspace V; x \<in> V |] ==> #-1 \<cdot> x = - x"
   by (unfold is_vectorspace_def) simp
 
 lemma diff_eq2: 
-  "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> x + - y = x - y"
+  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x + - y = x - y"
   by (unfold is_vectorspace_def) simp  
 
-lemma vs_not_empty [intro?]: "is_vectorspace V ==> (V \\<noteq> {})" 
+lemma vs_not_empty [intro?]: "is_vectorspace V ==> (V \<noteq> {})" 
   by (unfold is_vectorspace_def) simp
  
 lemma vs_add_closed [simp, intro?]: 
-  "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> x + y \\<in> V" 
+  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x + y \<in> V" 
   by (unfold is_vectorspace_def) simp
 
 lemma vs_mult_closed [simp, intro?]: 
-  "[| is_vectorspace V; x \\<in> V |] ==> a \\<cdot> x \\<in> V" 
+  "[| is_vectorspace V; x \<in> V |] ==> a \<cdot> x \<in> V" 
   by (unfold is_vectorspace_def) simp
 
 lemma vs_diff_closed [simp, intro?]: 
- "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> x - y \\<in> V"
+ "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x - y \<in> V"
   by (simp add: diff_eq1 negate_eq1)
 
 lemma vs_neg_closed  [simp, intro?]: 
-  "[| is_vectorspace V; x \\<in> V |] ==> - x \\<in> V"
+  "[| is_vectorspace V; x \<in> V |] ==> - x \<in> V"
   by (simp add: negate_eq1)
 
 lemma vs_add_assoc [simp]:  
-  "[| is_vectorspace V; x \\<in> V; y \\<in> V; z \\<in> V |]
+  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |]
    ==> (x + y) + z = x + (y + z)"
   by (unfold is_vectorspace_def) fast
 
 lemma vs_add_commute [simp]: 
-  "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> y + x = x + y"
+  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> y + x = x + y"
   by (unfold is_vectorspace_def) simp
 
 lemma vs_add_left_commute [simp]:
-  "[| is_vectorspace V; x \\<in> V; y \\<in> V; z \\<in> V |] 
+  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] 
   ==> x + (y + z) = y + (x + z)"
 proof -
-  assume "is_vectorspace V" "x \\<in> V" "y \\<in> V" "z \\<in> V"
+  assume "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V"
   hence "x + (y + z) = (x + y) + z" 
     by (simp only: vs_add_assoc)
   also have "... = (y + x) + z" by (simp! only: vs_add_commute)
@@ -139,78 +139,78 @@
 theorems vs_add_ac = vs_add_assoc vs_add_commute vs_add_left_commute
 
 lemma vs_diff_self [simp]: 
-  "[| is_vectorspace V; x \\<in> V |] ==>  x - x = 0" 
+  "[| is_vectorspace V; x \<in> V |] ==>  x - x = 0" 
   by (unfold is_vectorspace_def) simp
 
 text {* The existence of the zero element of a vector space
 follows from the non-emptiness of carrier set. *}
 
-lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> 0 \\<in> V"
+lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> 0 \<in> V"
 proof - 
   assume "is_vectorspace V"
-  have "V \\<noteq> {}" ..
-  hence "\\<exists>x. x \\<in> V" by force
+  have "V \<noteq> {}" ..
+  hence "\<exists>x. x \<in> V" by force
   thus ?thesis 
   proof 
-    fix x assume "x \\<in> V" 
+    fix x assume "x \<in> V" 
     have "0 = x - x" by (simp!)
-    also have "... \\<in> V" by (simp! only: vs_diff_closed)
+    also have "... \<in> V" by (simp! only: vs_diff_closed)
     finally show ?thesis .
   qed
 qed
 
 lemma vs_add_zero_left [simp]: 
-  "[| is_vectorspace V; x \\<in> V |] ==>  0 + x = x"
+  "[| is_vectorspace V; x \<in> V |] ==>  0 + x = x"
   by (unfold is_vectorspace_def) simp
 
 lemma vs_add_zero_right [simp]: 
-  "[| is_vectorspace V; x \\<in> V |] ==>  x + 0 = x"
+  "[| is_vectorspace V; x \<in> V |] ==>  x + 0 = x"
 proof -
-  assume "is_vectorspace V" "x \\<in> V"
+  assume "is_vectorspace V" "x \<in> V"
   hence "x + 0 = 0 + x" by simp
   also have "... = x" by (simp!)
   finally show ?thesis .
 qed
 
 lemma vs_add_mult_distrib1: 
-  "[| is_vectorspace V; x \\<in> V; y \\<in> V |] 
-  ==> a \\<cdot> (x + y) = a \\<cdot> x + a \\<cdot> y"
+  "[| is_vectorspace V; x \<in> V; y \<in> V |] 
+  ==> a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y"
   by (unfold is_vectorspace_def) simp
 
 lemma vs_add_mult_distrib2: 
-  "[| is_vectorspace V; x \\<in> V |] 
-  ==> (a + b) \\<cdot> x = a \\<cdot> x + b \\<cdot> x" 
+  "[| is_vectorspace V; x \<in> V |] 
+  ==> (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x" 
   by (unfold is_vectorspace_def) simp
 
 lemma vs_mult_assoc: 
-  "[| is_vectorspace V; x \\<in> V |] ==> (a * b) \\<cdot> x = a \\<cdot> (b \\<cdot> x)"
+  "[| is_vectorspace V; x \<in> V |] ==> (a * b) \<cdot> x = a \<cdot> (b \<cdot> x)"
   by (unfold is_vectorspace_def) simp
 
 lemma vs_mult_assoc2 [simp]: 
- "[| is_vectorspace V; x \\<in> V |] ==> a \\<cdot> b \\<cdot> x = (a * b) \\<cdot> x"
+ "[| is_vectorspace V; x \<in> V |] ==> a \<cdot> b \<cdot> x = (a * b) \<cdot> x"
   by (simp only: vs_mult_assoc)
 
 lemma vs_mult_1 [simp]: 
-  "[| is_vectorspace V; x \\<in> V |] ==> #1 \\<cdot> x = x" 
+  "[| is_vectorspace V; x \<in> V |] ==> #1 \<cdot> x = x" 
   by (unfold is_vectorspace_def) simp
 
 lemma vs_diff_mult_distrib1: 
-  "[| is_vectorspace V; x \\<in> V; y \\<in> V |] 
-  ==> a \\<cdot> (x - y) = a \\<cdot> x - a \\<cdot> y"
+  "[| is_vectorspace V; x \<in> V; y \<in> V |] 
+  ==> a \<cdot> (x - y) = a \<cdot> x - a \<cdot> y"
   by (simp add: diff_eq1 negate_eq1 vs_add_mult_distrib1)
 
 lemma vs_diff_mult_distrib2: 
-  "[| is_vectorspace V; x \\<in> V |] 
-  ==> (a - b) \\<cdot> x = a \\<cdot> x - (b \\<cdot> x)"
+  "[| is_vectorspace V; x \<in> V |] 
+  ==> (a - b) \<cdot> x = a \<cdot> x - (b \<cdot> x)"
 proof -
-  assume "is_vectorspace V" "x \\<in> V"
-  have " (a - b) \\<cdot> x = (a + - b) \\<cdot> x" 
+  assume "is_vectorspace V" "x \<in> V"
+  have " (a - b) \<cdot> x = (a + - b) \<cdot> x" 
     by (unfold real_diff_def, simp)
-  also have "... = a \\<cdot> x + (- b) \\<cdot> x" 
+  also have "... = a \<cdot> x + (- b) \<cdot> x" 
     by (rule vs_add_mult_distrib2)
-  also have "... = a \\<cdot> x + - (b \\<cdot> x)" 
+  also have "... = a \<cdot> x + - (b \<cdot> x)" 
     by (simp! add: negate_eq1)
-  also have "... = a \\<cdot> x - (b \\<cdot> x)" 
+  also have "... = a \<cdot> x - (b \<cdot> x)" 
     by (simp! add: diff_eq1)
   finally show ?thesis .
 qed
@@ -220,14 +220,14 @@
 text{* Further derived laws: *}
 
 lemma vs_mult_zero_left [simp]: 
-  "[| is_vectorspace V; x \\<in> V |] ==> #0 \\<cdot> x = 0"
+  "[| is_vectorspace V; x \<in> V |] ==> #0 \<cdot> x = 0"
 proof -
-  assume "is_vectorspace V" "x \\<in> V"
-  have  "#0 \\<cdot> x = (#1 - #1) \\<cdot> x" by simp
-  also have "... = (#1 + - #1) \\<cdot> x" by simp
-  also have "... =  #1 \\<cdot> x + (- #1) \\<cdot> x" 
+  assume "is_vectorspace V" "x \<in> V"
+  have  "#0 \<cdot> x = (#1 - #1) \<cdot> x" by simp
+  also have "... = (#1 + - #1) \<cdot> x" by simp
+  also have "... =  #1 \<cdot> x + (- #1) \<cdot> x" 
     by (rule vs_add_mult_distrib2)
-  also have "... = x + (- #1) \\<cdot> x" by (simp!)
+  also have "... = x + (- #1) \<cdot> x" by (simp!)
   also have "... = x + - x" by (simp! add: negate_eq2a)
   also have "... = x - x" by (simp! add: diff_eq2)
   also have "... = 0" by (simp!)
@@ -236,24 +236,24 @@
 
 lemma vs_mult_zero_right [simp]: 
   "[| is_vectorspace (V:: 'a::{plus, minus, zero} set) |] 
-  ==> a \\<cdot> 0 = (0::'a)"
+  ==> a \<cdot> 0 = (0::'a)"
 proof -
   assume "is_vectorspace V"
-  have "a \\<cdot> 0 = a \\<cdot> (0 - (0::'a))" by (simp!)
-  also have "... =  a \\<cdot> 0 - a \\<cdot> 0"
+  have "a \<cdot> 0 = a \<cdot> (0 - (0::'a))" by (simp!)
+  also have "... =  a \<cdot> 0 - a \<cdot> 0"
      by (rule vs_diff_mult_distrib1) (simp!)+
   also have "... = 0" by (simp!)
   finally show ?thesis .
 qed
 
 lemma vs_minus_mult_cancel [simp]:  
-  "[| is_vectorspace V; x \\<in> V |] ==> (- a) \\<cdot> - x = a \\<cdot> x"
+  "[| is_vectorspace V; x \<in> V |] ==> (- a) \<cdot> - x = a \<cdot> x"
   by (simp add: negate_eq1)
 
 lemma vs_add_minus_left_eq_diff: 
-  "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> - x + y = y - x"
+  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> - x + y = y - x"
 proof - 
-  assume "is_vectorspace V" "x \\<in> V" "y \\<in> V"
+  assume "is_vectorspace V" "x \<in> V" "y \<in> V"
   hence "- x + y = y + - x" 
     by (simp add: vs_add_commute)
   also have "... = y - x" by (simp! add: diff_eq1)
@@ -261,15 +261,15 @@
 qed
 
 lemma vs_add_minus [simp]: 
-  "[| is_vectorspace V; x \\<in> V |] ==> x + - x = 0"
+  "[| is_vectorspace V; x \<in> V |] ==> x + - x = 0"
   by (simp! add: diff_eq2)
 
 lemma vs_add_minus_left [simp]: 
-  "[| is_vectorspace V; x \\<in> V |] ==> - x + x = 0"
+  "[| is_vectorspace V; x \<in> V |] ==> - x + x = 0"
   by (simp! add: diff_eq2)
 
 lemma vs_minus_minus [simp]: 
-  "[| is_vectorspace V; x \\<in> V |] ==> - (- x) = x"
+  "[| is_vectorspace V; x \<in> V |] ==> - (- x) = x"
   by (simp add: negate_eq1)
 
 lemma vs_minus_zero [simp]: 
@@ -277,10 +277,10 @@
   by (simp add: negate_eq1)
 
 lemma vs_minus_zero_iff [simp]:
-  "[| is_vectorspace V; x \\<in> V |] ==> (- x = 0) = (x = 0)" 
+  "[| is_vectorspace V; x \<in> V |] ==> (- x = 0) = (x = 0)" 
   (concl is "?L = ?R")
 proof -
-  assume "is_vectorspace V" "x \\<in> V"
+  assume "is_vectorspace V" "x \<in> V"
   show "?L = ?R"
   proof
     have "x = - (- x)" by (simp! add: vs_minus_minus)
@@ -291,32 +291,32 @@
 qed
 
 lemma vs_add_minus_cancel [simp]:  
-  "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> x + (- x + y) = y" 
+  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x + (- x + y) = y" 
   by (simp add: vs_add_assoc [RS sym] del: vs_add_commute) 
 
 lemma vs_minus_add_cancel [simp]: 
-  "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> - x + (x + y) = y" 
+  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> - x + (x + y) = y" 
   by (simp add: vs_add_assoc [RS sym] del: vs_add_commute) 
 
 lemma vs_minus_add_distrib [simp]:  
-  "[| is_vectorspace V; x \\<in> V; y \\<in> V |] 
+  "[| is_vectorspace V; x \<in> V; y \<in> V |] 
   ==> - (x + y) = - x + - y"
   by (simp add: negate_eq1 vs_add_mult_distrib1)
 
 lemma vs_diff_zero [simp]: 
-  "[| is_vectorspace V; x \\<in> V |] ==> x - 0 = x"
+  "[| is_vectorspace V; x \<in> V |] ==> x - 0 = x"
   by (simp add: diff_eq1)  
 
 lemma vs_diff_zero_right [simp]: 
-  "[| is_vectorspace V; x \\<in> V |] ==> 0 - x = - x"
+  "[| is_vectorspace V; x \<in> V |] ==> 0 - x = - x"
   by (simp add:diff_eq1)
 
 lemma vs_add_left_cancel:
-  "[| is_vectorspace V; x \\<in> V; y \\<in> V; z \\<in> V |] 
+  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] 
    ==> (x + y = x + z) = (y = z)"  
   (concl is "?L = ?R")
 proof
-  assume "is_vectorspace V" "x \\<in> V" "y \\<in> V" "z \\<in> V"
+  assume "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V"
   have "y = 0 + y" by (simp!)
   also have "... = - x + x + y" by (simp!)
   also have "... = - x + (x + y)" 
@@ -329,67 +329,67 @@
 qed force
 
 lemma vs_add_right_cancel: 
-  "[| is_vectorspace V; x \\<in> V; y \\<in> V; z \\<in> V |] 
+  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] 
   ==> (y + x = z + x) = (y = z)"  
   by (simp only: vs_add_commute vs_add_left_cancel)
 
 lemma vs_add_assoc_cong: 
-  "[| is_vectorspace V; x \\<in> V; y \\<in> V; x' \\<in> V; y' \\<in> V; z \\<in> V |] 
+  "[| is_vectorspace V; x \<in> V; y \<in> V; x' \<in> V; y' \<in> V; z \<in> V |] 
   ==> x + y = x' + y' ==> x + (y + z) = x' + (y' + z)"
   by (simp only: vs_add_assoc [RS sym]) 
 
 lemma vs_mult_left_commute: 
-  "[| is_vectorspace V; x \\<in> V; y \\<in> V; z \\<in> V |] 
-  ==> x \\<cdot> y \\<cdot> z = y \\<cdot> x \\<cdot> z"  
+  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] 
+  ==> x \<cdot> y \<cdot> z = y \<cdot> x \<cdot> z"  
   by (simp add: real_mult_commute)
 
 lemma vs_mult_zero_uniq:
-  "[| is_vectorspace V; x \\<in> V; a \\<cdot> x = 0; x \\<noteq> 0 |] ==> a = #0"
+  "[| is_vectorspace V; x \<in> V; a \<cdot> x = 0; x \<noteq> 0 |] ==> a = #0"
 proof (rule classical)
-  assume "is_vectorspace V" "x \\<in> V" "a \\<cdot> x = 0" "x \\<noteq> 0"
-  assume "a \\<noteq> #0"
-  have "x = (rinv a * a) \\<cdot> x" by (simp!)
-  also have "... = rinv a \\<cdot> (a \\<cdot> x)" by (rule vs_mult_assoc)
-  also have "... = rinv a \\<cdot> 0" by (simp!)
+  assume "is_vectorspace V" "x \<in> V" "a \<cdot> x = 0" "x \<noteq> 0"
+  assume "a \<noteq> #0"
+  have "x = (rinv a * a) \<cdot> x" by (simp!)
+  also have "... = rinv a \<cdot> (a \<cdot> x)" by (rule vs_mult_assoc)
+  also have "... = rinv a \<cdot> 0" by (simp!)
   also have "... = 0" by (simp!)
   finally have "x = 0" .
   thus "a = #0" by contradiction 
 qed
 
 lemma vs_mult_left_cancel: 
-  "[| is_vectorspace V; x \\<in> V; y \\<in> V; a \\<noteq> #0 |] ==> 
-  (a \\<cdot> x = a \\<cdot> y) = (x = y)"
+  "[| is_vectorspace V; x \<in> V; y \<in> V; a \<noteq> #0 |] ==> 
+  (a \<cdot> x = a \<cdot> y) = (x = y)"
   (concl is "?L = ?R")
 proof
-  assume "is_vectorspace V" "x \\<in> V" "y \\<in> V" "a \\<noteq> #0"
-  have "x = #1 \\<cdot> x" by (simp!)
-  also have "... = (rinv a * a) \\<cdot> x" by (simp!)
-  also have "... = rinv a \\<cdot> (a \\<cdot> x)" 
+  assume "is_vectorspace V" "x \<in> V" "y \<in> V" "a \<noteq> #0"
+  have "x = #1 \<cdot> x" by (simp!)
+  also have "... = (rinv a * a) \<cdot> x" by (simp!)
+  also have "... = rinv a \<cdot> (a \<cdot> x)" 
     by (simp! only: vs_mult_assoc)
   also assume ?L
-  also have "rinv a \\<cdot> ... = y" by (simp!)
+  also have "rinv a \<cdot> ... = y" by (simp!)
   finally show ?R .
 qed simp
 
 lemma vs_mult_right_cancel: (*** forward ***)
-  "[| is_vectorspace V; x \\<in> V; x \\<noteq> 0 |] 
-  ==> (a \\<cdot> x = b \\<cdot> x) = (a = b)" (concl is "?L = ?R")
+  "[| is_vectorspace V; x \<in> V; x \<noteq> 0 |] 
+  ==> (a \<cdot> x = b \<cdot> x) = (a = b)" (concl is "?L = ?R")
 proof
-  assume "is_vectorspace V" "x \\<in> V" "x \\<noteq> 0"
-  have "(a - b) \\<cdot> x = a \\<cdot> x - b \\<cdot> x" 
+  assume "is_vectorspace V" "x \<in> V" "x \<noteq> 0"
+  have "(a - b) \<cdot> x = a \<cdot> x - b \<cdot> x" 
     by (simp! add: vs_diff_mult_distrib2)
-  also assume ?L hence "a \\<cdot> x - b \\<cdot> x = 0" by (simp!)
-  finally have "(a - b) \\<cdot> x = 0" . 
+  also assume ?L hence "a \<cdot> x - b \<cdot> x = 0" by (simp!)
+  finally have "(a - b) \<cdot> x = 0" . 
   hence "a - b = #0" by (simp! add: vs_mult_zero_uniq)
   thus "a = b" by (rule real_add_minus_eq)
 qed simp (*** 
 
 lemma vs_mult_right_cancel: 
-  "[| is_vectorspace V; x:V; x \\<noteq> 0 |] ==>  
+  "[| is_vectorspace V; x:V; x \<noteq> 0 |] ==>  
   (a ( * ) x = b ( * ) x) = (a = b)"
   (concl is "?L = ?R");
 proof;
-  assume "is_vectorspace V" "x:V" "x \\<noteq> 0";
+  assume "is_vectorspace V" "x:V" "x \<noteq> 0";
   assume l: ?L; 
   show "a = b"; 
   proof (rule real_add_minus_eq);
@@ -408,11 +408,11 @@
 **)
 
 lemma vs_eq_diff_eq: 
-  "[| is_vectorspace V; x \\<in> V; y \\<in> V; z \\<in> V |] ==> 
+  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] ==> 
   (x = z - y) = (x + y = z)"
   (concl is "?L = ?R" )  
 proof -
-  assume vs: "is_vectorspace V" "x \\<in> V" "y \\<in> V" "z \\<in> V"
+  assume vs: "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V"
   show "?L = ?R"   
   proof
     assume ?L
@@ -437,9 +437,9 @@
 qed
 
 lemma vs_add_minus_eq_minus: 
-  "[| is_vectorspace V; x \\<in> V; y \\<in> V; x + y = 0 |] ==> x = - y" 
+  "[| is_vectorspace V; x \<in> V; y \<in> V; x + y = 0 |] ==> x = - y" 
 proof -
-  assume "is_vectorspace V" "x \\<in> V" "y \\<in> V" 
+  assume "is_vectorspace V" "x \<in> V" "y \<in> V" 
   have "x = (- y + y) + x" by (simp!)
   also have "... = - y + (x + y)" by (simp!)
   also assume "x + y = 0"
@@ -448,9 +448,9 @@
 qed
 
 lemma vs_add_minus_eq: 
-  "[| is_vectorspace V; x \\<in> V; y \\<in> V; x - y = 0 |] ==> x = y" 
+  "[| is_vectorspace V; x \<in> V; y \<in> V; x - y = 0 |] ==> x = y" 
 proof -
-  assume "is_vectorspace V" "x \\<in> V" "y \\<in> V" "x - y = 0"
+  assume "is_vectorspace V" "x \<in> V" "y \<in> V" "x - y = 0"
   assume "x - y = 0"
   hence e: "x + - y = 0" by (simp! add: diff_eq1)
   with _ _ _ have "x = - (- y)" 
@@ -459,10 +459,10 @@
 qed
 
 lemma vs_add_diff_swap:
-  "[| is_vectorspace V; a \\<in> V; b \\<in> V; c \\<in> V; d \\<in> V; a + b = c + d |] 
+  "[| is_vectorspace V; a \<in> V; b \<in> V; c \<in> V; d \<in> V; a + b = c + d |] 
   ==> a - c = d - b"
 proof - 
-  assume vs: "is_vectorspace V" "a \\<in> V" "b \\<in> V" "c \\<in> V" "d \\<in> V" 
+  assume vs: "is_vectorspace V" "a \<in> V" "b \<in> V" "c \<in> V" "d \<in> V" 
     and eq: "a + b = c + d"
   have "- c + (a + b) = - c + (c + d)" 
     by (simp! add: vs_add_left_cancel)
@@ -477,11 +477,11 @@
 qed
 
 lemma vs_add_cancel_21: 
-  "[| is_vectorspace V; x \\<in> V; y \\<in> V; z \\<in> V; u \\<in> V |] 
+  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V; u \<in> V |] 
   ==> (x + (y + z) = y + u) = ((x + z) = u)"
   (concl is "?L = ?R") 
 proof - 
-  assume "is_vectorspace V" "x \\<in> V" "y \\<in> V" "z \\<in> V" "u \\<in> V"
+  assume "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V" "u \<in> V"
   show "?L = ?R"
   proof
     have "x + z = - y + y + (x + z)" by (simp!)
@@ -495,11 +495,11 @@
 qed
 
 lemma vs_add_cancel_end: 
-  "[| is_vectorspace V; x \\<in> V; y \\<in> V; z \\<in> V |] 
+  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] 
   ==> (x + (y + z) = y) = (x = - z)"
   (concl is "?L = ?R" )
 proof -
-  assume "is_vectorspace V" "x \\<in> V" "y \\<in> V" "z \\<in> V"
+  assume "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V"
   show "?L = ?R"
   proof
     assume l: ?L
diff -r 50ec59aff389 -r 3324cbbecef8 src/HOL/ex/Tuple.thy
--- a/src/HOL/ex/Tuple.thy	Wed Aug 02 19:40:14 2000 +0200
+++ b/src/HOL/ex/Tuple.thy	Thu Aug 03 00:34:22 2000 +0200
@@ -37,12 +37,12 @@
   "_tuple_type"      :: "type => tuple_type_args => type"            ("(_ */ _)" [21, 20] 20)
 
 syntax (symbols)
-  "_tuple_type_args" :: "type => tuple_type_args => tuple_type_args" ("_ \\<times>/ _" [21, 20] 20)
-  "_tuple_type"      :: "type => tuple_type_args => type"          ("(_ \\<times>/ _)" [21, 20] 20)
+  "_tuple_type_args" :: "type => tuple_type_args => tuple_type_args" ("_ \<times>/ _" [21, 20] 20)
+  "_tuple_type"      :: "type => tuple_type_args => type"          ("(_ \<times>/ _)" [21, 20] 20)
 
 syntax (HTML output)
-  "_tuple_type_args" :: "type => tuple_type_args => tuple_type_args" ("_ \\<times>/ _" [21, 20] 20)
-  "_tuple_type"      :: "type => tuple_type_args => type"          ("(_ \\<times>/ _)" [21, 20] 20)
+  "_tuple_type_args" :: "type => tuple_type_args => tuple_type_args" ("_ \<times>/ _" [21, 20] 20)
+  "_tuple_type"      :: "type => tuple_type_args => type"          ("(_ \<times>/ _)" [21, 20] 20)
 
 translations
   (type) "'a * 'b" == (type) "('a, ('b, unit) prod) prod"