# HG changeset patch
# User bauerg
# Date 963835098 -7200
# Node ID 153853af318b234eb1a3a34e7861d07c0ffcfe41
# Parent  78a11a3534737089b39f8acceb62837e49a30309
- xsymbols for
  \<noteq> \<notin> \<in> \<exists> \<forall>
  \<and> \<inter> \<union> \<Union>
- vector space type of {plus, minus, zero},  overload 0 in vector space
- syntax |.| and ||.||

diff -r 78a11a353473 -r 153853af318b src/HOL/Real/HahnBanach/Aux.thy
--- a/src/HOL/Real/HahnBanach/Aux.thy	Sun Jul 16 21:00:32 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Aux.thy	Mon Jul 17 13:58:18 2000 +0200
@@ -17,22 +17,22 @@
 text_raw {* \medskip *}
 text{* Lemmas about sets. *}
 
-lemma Int_singletonD: "[| A Int B = {v}; x:A; x: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 ==> EX x0:E. x0 ~: 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 ~= y" 
+lemma lt_imp_not_eq: "x < (y::'a::order) ==> x \<noteq> y" 
   by (rule order_less_le[RS iffD1, RS conjunct2])
 
 lemma le_noteq_imp_less: 
-  "[| x <= (r::'a::order); x ~= r |] ==> x < r"
+  "[| x <= (r::'a::order); x \<noteq> r |] ==> x < r"
 proof -
-  assume "x <= (r::'a::order)" and ne:"x ~= 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
@@ -116,10 +116,10 @@
   thus ?thesis; by simp;
 qed;
 
-lemma real_mult_inv_right1: "x ~= #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 ~= #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 78a11a353473 -r 153853af318b src/HOL/Real/HahnBanach/Bounds.thy
--- a/src/HOL/Real/HahnBanach/Bounds.thy	Sun Jul 16 21:00:32 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Bounds.thy	Mon Jul 17 13:58:18 2000 +0200
@@ -11,13 +11,13 @@
 
 constdefs
   is_LowerBound :: "('a::order) set => 'a set => 'a => bool"
-  "is_LowerBound A B == \<lambda>x. x:A & (ALL y: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:A & (ALL y: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)"
@@ -70,7 +70,7 @@
 text {*
  A supremum\footnote{The definition of the supremum is based on one in
  \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Lubs.html}}  of
- an ordered set $B$ w.~r.~t.~$A$ is defined as a least upper bound of
+ an ordered set $B$ w.~r.~.~ $A$ is defined as a least upper bound of
  $B$, which lies in $A$.
 *}
    
@@ -86,7 +86,7 @@
 (*<*)
 constdefs
   is_Inf :: "('a::order) set => 'a set => 'a => bool"
-  "is_Inf A B x == x:A & 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)"
@@ -115,16 +115,16 @@
 
 text {* The supremum $B$ is an upper bound for $B$. *}
 
-lemma sup_ub: "y: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: 
-  "[| ALL y:B. a <= y; is_Sup A B s; x:B |] ==> a <= s"
+  "[| \<forall> y \<in> B. a <= y; is_Sup A B s; x \<in> B |] ==> a <= s"
 proof - 
-  assume "ALL y:B. a <= y" "is_Sup A B s" "x: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 78a11a353473 -r 153853af318b src/HOL/Real/HahnBanach/FunctionNorm.thy
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Sun Jul 16 21:00:32 2000 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Mon Jul 17 13:58:18 2000 +0200
@@ -18,16 +18,16 @@
 
 constdefs
   is_continuous ::
-  "['a::{minus, plus} set, 'a => real, 'a => real] => bool" 
+  "['a::{plus, minus, zero} set, 'a => real, 'a => real] => bool" 
   "is_continuous V norm f == 
-    is_linearform V f & (EX c. ALL x:V. abs (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:V ==> abs (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:V ==> abs (f x) <= c * norm x" 
-  fix x assume "x:V" show "abs (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 
-  ==> EX c. ALL x:V. abs (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 *}
@@ -59,14 +59,14 @@
 
 Thus we define the set $B$ the supremum is taken from as
 \[
-\{ 0 \} \Un \left\{ \frac{|f\ap x|}{\norm x} \dt x\neq \zero \And x\in F\right\}
+\{ 0 \} \Union \left\{ \frac{|f\ap x|}{\norm x} \dt x\neq \zero \And x\in F\right\}
  \]
 *}
 
 constdefs
-  B :: "[ 'a set, 'a => real, 'a => real ] => real set"
+  B :: "[ 'a set, 'a => real, 'a::{plus, minus, zero} => real ] => real set"
   "B V norm f == 
-  {#0} Un {abs (f x) * rinv (norm x) | x. x ~= 00 & x: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$. 
@@ -74,17 +74,20 @@
 
 constdefs 
   is_function_norm :: 
-  " ['a set, 'a => real, 'a => real] => real => bool"
-  "is_function_norm V norm f fn == is_Sup UNIV (B V norm f) fn"
+  " ['a::{minus,plus,zero}  => real, 'a set, 'a => real] => real => bool"
+  "is_function_norm f V norm fn == is_Sup UNIV (B V norm f) fn"
 
 text{* $\idt{function{\dsh}norm}$ is equal to the supremum of $B$, 
 if the supremum exists. Otherwise it is undefined. *}
 
 constdefs 
-  function_norm :: " ['a set, 'a => real, 'a => real] => real"
-  "function_norm V norm f == Sup UNIV (B V norm f)"
+  function_norm :: " ['a::{minus,plus,zero} => real, 'a set, 'a => real] => real"
+  "function_norm f V norm == Sup UNIV (B V norm f)"
 
-lemma B_not_empty: "#0 : B V norm f"
+syntax   
+  function_norm :: " ['a => real, 'a set, 'a => real] => real" ("\<parallel>_\<parallel>_,_")
+
+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
@@ -92,35 +95,35 @@
 
 lemma ex_fnorm [intro??]: 
   "[| is_normed_vectorspace V norm; is_continuous V norm f|]
-     ==> is_function_norm V norm f (function_norm V norm f)" 
+     ==> 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: "EX c. ALL x:V. abs (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  "EX 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 "EX X. X : B V norm f" 
+    show "\<exists>X. X \<in> B V norm f" 
     proof (intro exI)
-      show "#0 : (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 "EX 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: "ALL x:V. abs (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"
@@ -141,7 +144,7 @@
 
       next
 	fix x y
-        assume "x:V" "x ~= 00" (***
+        assume "x \<in> V" "x \<noteq> 0" (***
 
          have ge: "#0 <= rinv (norm x)";
           by (rule real_less_imp_le, rule real_rinv_gt_zero, 
@@ -152,11 +155,11 @@
               show "#0 < norm x"; ..;
             qed;
           qed; *** )
-        have nz: "norm x ~= #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 ~= norm x"; 
+            show "#0 \<noteq> norm x"; 
             proof (rule lt_imp_not_eq);
               show "#0 < norm x"; ..;
             qed;
@@ -165,19 +168,19 @@
         txt {* The thesis follows by a short calculation using the 
         fact that $f$ is bounded. *}
     
-        assume "y = abs (f x) * rinv (norm x)"
+        assume "y = |f x| * rinv (norm x)"
         also have "... <= c * norm x * rinv (norm x)"
         proof (rule real_mult_le_le_mono2)
           show "#0 <= rinv (norm x)"
             by (rule real_less_imp_le, rule real_rinv_gt_zero1, 
                 rule normed_vs_norm_gt_zero)
-          from a show "abs (f x) <= c * norm x" ..
+          from a show "|f x| <= c * norm x" ..
         qed
         also have "... = c * (norm x * rinv (norm x))" 
           by (rule real_mult_assoc)
         also have "(norm x * rinv (norm x)) = (#1::real)" 
         proof (rule real_mult_inv_right1)
-          show nz: "norm x ~= #0" 
+          show nz: "norm x \<noteq> #0" 
             by (rule not_sym, rule lt_imp_not_eq, 
               rule normed_vs_norm_gt_zero)
         qed
@@ -191,8 +194,8 @@
 text {* The norm of a continuous function is always $\geq 0$. *}
 
 lemma fnorm_ge_zero [intro??]: 
-  "[| is_continuous V norm f; is_normed_vectorspace V norm|]
-   ==> #0 <= function_norm V norm f"
+  "[| is_continuous V norm f; is_normed_vectorspace V norm |]
+   ==> #0 <= \<parallel>f\<parallel>V,norm"
 proof -
   assume c: "is_continuous V norm f" 
      and n: "is_normed_vectorspace V norm"
@@ -203,14 +206,14 @@
 
   show ?thesis 
   proof (unfold function_norm_def, rule sup_ub1)
-    show "ALL x:(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 : V" "x ~= 00" 
-        and r: "r = abs (f x) * rinv (norm x)"
+      assume "x \<in> V" "x \<noteq> 0" 
+        and r: "r = |f x| * rinv (norm x)"
 
-      have ge: "#0 <= abs (f x)" by (simp! only: abs_ge_zero)
+      have ge: "#0 <= |f x|" by (simp! only: abs_ge_zero)
       have "#0 <= rinv (norm x)" 
         by (rule real_less_imp_le, rule real_rinv_gt_zero1, rule)(***
         proof (rule real_less_imp_le);
@@ -225,13 +228,13 @@
 
     txt {* Since $f$ is continuous the function norm exists: *}
 
-    have "is_function_norm V norm f (function_norm V norm f)" ..
+    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 : B V norm f" by (rule B_not_empty)
+    show "#0 \<in> B V norm f" by (rule B_not_empty)
   qed
 qed
   
@@ -242,13 +245,12 @@
 *}
 
 lemma norm_fx_le_norm_f_norm_x: 
-  "[| is_normed_vectorspace V norm; x:V; is_continuous V norm f |] 
-    ==> abs (f x) <= function_norm V 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"
 proof - 
-  assume "is_normed_vectorspace V norm" "x:V" 
+  assume "is_normed_vectorspace V norm" "x \<in> V" 
   and c: "is_continuous V norm f"
   have v: "is_vectorspace V" ..
-  assume "x:V"
 
  txt{* The proof is by case analysis on $x$. *}
  
@@ -259,22 +261,22 @@
     from the linearity of $f$: for every linear function
     holds $f\ap \zero = 0$. *}
 
-    assume "x = 00"
-    have "abs (f x) = abs (f 00)" by (simp!)
-    also from v continuous_linearform have "f 00 = #0" ..
+    assume "x = 0"
+    have "|f x| = |f 0|" by (simp!)
+    also from v continuous_linearform have "f 0 = #0" ..
     also note abs_zero
-    also have "#0 <= function_norm V norm f * norm x"
+    also have "#0 <= \<parallel>f\<parallel>V,norm * norm x"
     proof (rule real_le_mult_order1a)
-      show "#0 <= function_norm V norm f" ..
+      show "#0 <= \<parallel>f\<parallel>V,norm" ..
       show "#0 <= norm x" ..
     qed
     finally 
-    show "abs (f x) <= function_norm V norm f * norm x" .
+    show "|f x| <= \<parallel>f\<parallel>V,norm * norm x" .
 
   next
-    assume "x ~= 00"
+    assume "x \<noteq> 0"
     have n: "#0 <= norm x" ..
-    have nz: "norm x ~= #0"
+    have nz: "norm x \<noteq> #0"
     proof (rule lt_imp_not_eq [RS not_sym])
       show "#0 < norm x" ..
     qed
@@ -282,28 +284,28 @@
     txt {* For the case $x\neq \zero$ we derive the following
     fact from the definition of the function norm:*}
 
-    have l: "abs (f x) * rinv (norm x) <= function_norm V norm f"
+    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 "abs (f x) * rinv (norm x) : 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
 
     txt {* The thesis now follows by a short calculation: *}
 
-    have "abs (f x) = abs (f x) * (#1::real)" by (simp!)
-    also from nz have "(#1::real) = rinv (norm x) * norm x" 
+    have "|f x| = |f x| * #1" by (simp!)
+    also from nz have "#1 = rinv (norm x) * norm x" 
       by (rule real_mult_inv_left1 [RS sym])
     also 
-    have "abs (f x) * ... = abs (f x) * rinv (norm x) * norm x"
-      by (simp! add: real_mult_assoc [of "abs (f x)"])
-    also have "... <= function_norm V norm f * norm x" 
+    have "|f x| * ... = |f x| * rinv (norm x) * norm x"
+      by (simp! add: real_mult_assoc)
+    also have "... <= \<parallel>f\<parallel>V,norm * norm x"
       by (rule real_mult_le_le_mono2 [OF n l])
     finally 
-    show "abs (f x) <= function_norm V norm f * norm x" .
+    show "|f x| <= \<parallel>f\<parallel>V,norm * norm x" .
   qed
 qed
 
@@ -315,13 +317,13 @@
 *}
 
 lemma fnorm_le_ub: 
-  "[| is_normed_vectorspace V norm; is_continuous V norm f;
-     ALL x:V. abs (f x) <= c * norm x; #0 <= c |]
-  ==> function_norm V norm f <= c"
+  "[| 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"
 proof (unfold function_norm_def)
   assume "is_normed_vectorspace V norm" 
   assume c: "is_continuous V norm f"
-  assume fb: "ALL x:V. abs (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$.
@@ -336,12 +338,12 @@
     show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))" 
       by (simp! add: is_function_norm_def function_norm_def) 
   
-    txt {* $c$ is an upper bound of $B$, i.~e.~every
+    txt {* $c$ is an upper bound of $B$, i.e. every
     $y\in B$ is less than $c$. *}
 
     show "isUb UNIV (B V norm f) c"  
     proof (intro isUbI setleI ballI)
-      fix y assume "y: 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)
 
@@ -356,14 +358,14 @@
 
       next
 	fix x 
-        assume "x : V" "x ~= 00" 
+        assume "x \<in> V" "x \<noteq> 0" 
 
         have lz: "#0 < norm x" 
           by (simp! add: normed_vs_norm_gt_zero)
           
-        have nz: "norm x ~= #0" 
+        have nz: "norm x \<noteq> #0" 
         proof (rule not_sym)
-          from lz show "#0 ~= norm x"
+          from lz show "#0 \<noteq> norm x"
             by (simp! add: order_less_imp_not_eq)
         qed
             
@@ -372,10 +374,10 @@
 	hence rinv_gez: "#0 <= rinv (norm x)"
           by (rule real_less_imp_le)
 
-	assume "y = abs (f x) * rinv (norm x)" 
+	assume "y = |f x| * rinv (norm x)" 
 	also from rinv_gez have "... <= c * norm x * rinv (norm x)"
 	  proof (rule real_mult_le_le_mono2)
-	    show "abs (f x) <= c * norm x" by (rule bspec)
+	    show "|f x| <= c * norm x" by (rule bspec)
 	  qed
 	also have "... <= c" by (simp add: nz real_mult_assoc)
 	finally show ?thesis .
diff -r 78a11a353473 -r 153853af318b src/HOL/Real/HahnBanach/FunctionOrder.thy
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Sun Jul 16 21:00:32 2000 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Mon Jul 17 13:58:18 2000 +0200
@@ -12,7 +12,7 @@
 text{* We define the \emph{graph} of a (real) function $f$ with
 domain $F$ as the set 
 \[
-\{(x, f\ap x). \ap x:F\}
+\{(x, f\ap x). \ap x \in F\}
 \]
 So we are modeling partial functions by specifying the domain and 
 the mapping function. We use the term ``function'' also for its graph.
@@ -22,18 +22,18 @@
 
 constdefs
   graph :: "['a set, 'a => real] => 'a graph "
-  "graph F f == {(x, f x) | x. x:F}" 
+  "graph F f == {(x, f x) | x. x \<in> F}" 
 
-lemma graphI [intro??]: "x:F ==> (x, f x) : 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:F ==> EX t: (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): graph F f ==> x: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): 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: 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: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,10 +61,10 @@
 
 constdefs
   domain :: "'a graph => 'a set" 
-  "domain g == {x. EX y. (x, y):g}"
+  "domain g == {x. \<exists>y. (x, y) \<in> g}"
 
   funct :: "'a graph => ('a => real)"
-  "funct g == \<lambda>x. (SOME y. (x, y):g)"
+  "funct g == \<lambda>x. (SOME y. (x, y) \<in> g)"
 
 (*text{*  The equations 
 \begin{matharray}
@@ -78,16 +78,16 @@
 if the relation induced by $g$ is unique. *}
 
 lemma graph_domain_funct: 
-  "(!!x y z. (x, y):g ==> (x, z):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) : g"
-  show "(a, SOME y. (a, y) : g) : g" by (rule selectI2)
-  show "EX y. (a, y) : g" ..
-  assume uniq: "!!x y z. (x, y):g ==> (x, z):g ==> z = y"
-  show "b = (SOME y. (a, y) : 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):g" show "y = b" by (rule uniq)
+    fix y assume "(a, y) \<in> g" show "y = b" by (rule uniq)
   qed
 qed
 
@@ -102,40 +102,40 @@
 
 constdefs
   norm_pres_extensions :: 
-    "['a::{minus, plus} set, 'a  => real, 'a set, 'a => real] 
+    "['a::{plus, minus, zero} set, 'a  => real, 'a set, 'a => real] 
     => 'a graph set"
     "norm_pres_extensions E p F f 
-    == {g. EX H h. graph H h = g 
-                & is_linearform H h 
-                & is_subspace H E
-                & is_subspace F H
-                & graph F f <= graph H h
-                & (ALL x: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 : norm_pres_extensions E p F f
-  ==> EX H h. graph H h = g 
-            & is_linearform H h 
-            & is_subspace H E
-            & is_subspace F H
-            & graph F f <= graph H h
-            & (ALL x: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; ALL x:H. h x <= p x |]
-  ==> (graph H h : 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]:  
-  "EX H h. graph H h = g 
-         & is_linearform H h    
-         & is_subspace H E
-         & is_subspace F H
-         & graph F f <= graph H h
-         & (ALL x:H. h x <= p x)
-  ==> g: 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 78a11a353473 -r 153853af318b src/HOL/Real/HahnBanach/HahnBanach.thy
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Sun Jul 16 21:00:32 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Mon Jul 17 13:58:18 2000 +0200
@@ -1,123 +1,182 @@
-theory HahnBanach = HahnBanachLemmas: text_raw {* \smallskip\\ *} (* from ~/Pub/TYPES99/HB/HahnBanach.thy *)
+(*  Title:      HOL/Real/HahnBanach/HahnBanach.thy
+    ID:         $Id$
+    Author:     Gertrud Bauer, TU Munich
+*)
+
+header {* The Hahn-Banach Theorem *}
+
+theory HahnBanach = HahnBanachLemmas: 
+
+text {*
+  We present the proof of two different versions of the Hahn-Banach 
+  Theorem, closely following \cite[\S36]{Heuser:1986}.
+*}
+
+subsection {* The Hahn-Banach Theorem for vector spaces *}
+
+text {*
+{\bf Hahn-Banach Theorem.}\quad
+  Let $F$ be a subspace of a real vector space $E$, let $p$ be a semi-norm on
+  $E$, and $f$ be a linear form defined on $F$ such that $f$ is bounded by
+  $p$, i.e. $\All {x\in F} f\ap x \leq p\ap x$.  Then $f$ can be extended to
+  a linear form $h$ on $E$ such that $h$ is norm-preserving, i.e. $h$ is also
+  bounded by $p$.
+
+\bigskip
+{\bf Proof Sketch.}
+\begin{enumerate}
+\item Define $M$ as the set of norm-preserving extensions of $f$ to subspaces
+  of $E$. The linear forms in $M$ are ordered by domain extension.
+\item We show that every non-empty chain in $M$ has an upper bound in $M$.
+\item With Zorn's Lemma we conclude that there is a maximal function $g$ in
+  $M$.
+\item The domain $H$ of $g$ is the whole space $E$, as shown by classical
+  contradiction:
+\begin{itemize}
+\item Assuming $g$ is not defined on whole $E$, it can still be extended in a
+  norm-preserving way to a super-space $H'$ of $H$.
+\item Thus $g$ can not be maximal. Contradiction!
+\end{itemize}
+\end{enumerate}
+\bigskip
+*}
+
+(*
+text {* {\bf Theorem.} Let $f$ be a linear form defined on a subspace 
+ $F$ of a real vector space $E$, such that $f$ is bounded by a seminorm 
+ $p$. 
+
+ Then $f$ can be extended  to a linear form $h$  on $E$ that is again
+ bounded by $p$.
+
+ \bigskip{\bf Proof Outline.}
+ First we define the set $M$ of all norm-preserving extensions of $f$.
+ We show that every chain in $M$ has an upper bound in $M$.
+ With Zorn's lemma we can conclude that $M$ has a maximal element $g$.
+ We further show by contradiction that the domain $H$ of $g$ is the whole
+ vector space $E$. 
+ If $H \neq E$, then $g$ can be extended in 
+ a norm-preserving way to a greater vector space $H_0$. 
+ So $g$ cannot be maximal in $M$.
+ \bigskip
+*}
+*)
 
 theorem HahnBanach:
-  "is_vectorspace E \\<Longrightarrow> is_subspace F E \\<Longrightarrow> is_seminorm E p
-  \\<Longrightarrow> is_linearform F f \\<Longrightarrow> \\<forall>x \\<in> F. f x \\<le> p x
-  \\<Longrightarrow> \\<exists>h. is_linearform E h \\<and> (\\<forall>x \\<in> F. h x = f x) \\<and> (\\<forall>x \\<in> E. h x \\<le> p x)"   
+  "[| is_vectorspace E; is_subspace F E; is_seminorm E p;
+  is_linearform F f; \<forall>x \<in> F. f x \<le> p x |] 
+  ==> \<exists>h. is_linearform E h \<and> (\<forall>x \<in> F. h x = f x) \<and> (\<forall>x \<in> E. h x \<le> 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 \\<le> p x"
+   and "is_linearform F f" "\<forall>x \<in> F. f x \<le> 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"
-    txt {* Show that every non-empty chain $c$ of $M$ has an upper bound in $M$: *}
-    txt {* $\Union c$ is greater than any element of the chain $c$, so it suffices to show $\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
-              & 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 \\<le> 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 \<le> 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" 
           by (simp! add: sup_lf a)
-        show "is_subspace ?H E" thm sup_subE [OF _ _ _ a]
-          by (rule sup_subE [OF _ _ _ a]) (simp !)+
-  (*  FIXME       by (rule sup_subE, rule a) (simp!)+; *)
+        show "is_subspace ?H E" 
+          by (rule sup_subE, rule a) (simp!)+
         show "is_subspace F ?H" 
-          by (rule sup_supF [OF _ _ _ a]) (simp!)+
-  (* FIXME        by (rule sup_supF, rule a) (simp!)+ *)
-        show "graph F f \\<subseteq> graph ?H ?h" 
-          by (rule sup_ext [OF _ _ _ a]) (simp!)+
-  (*  FIXME      by (rule sup_ext, rule a) (simp!)+*)
-        show "\\<forall>x \\<in> ?H. ?h x \\<le> p x" 
-          by (rule sup_norm_pres [OF _ _ a]) (simp!)+
-  (* FIXME        by (rule sup_norm_pres, rule a) (simp!)+ *)
+          by (rule sup_supF, rule a) (simp!)+
+        show "graph F f \<subseteq> graph ?H ?h" 
+          by (rule sup_ext, rule a) (simp!)+
+        show "\<forall>x \<in> ?H. ?h x \<le> p x" 
+          by (rule sup_norm_pres, rule a) (simp!)+
       qed
     qed
 
   }
-  hence "\\<exists>g \\<in> M. \\<forall>x \\<in> M. g \\<subseteq> x \\<longrightarrow> g = x" 
-  txt {* With Zorn's Lemma we can conclude that there is a maximal element in $M$.\skp *}
+  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)
-    txt {* We show that $M$ is non-empty: *}
-    have "graph F f \\<in> norm_pres_extensions E p F f"
+    -- {* We show that $M$ is non-empty: *}
+    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 \\<longrightarrow> 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 *}
     show ?thesis
       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 \\<le> p x" 
-        txt {* $g$ is a norm-preserving extension of $f$, in other words: *}
-        txt {* $g$ is the graph of some linear form $h$ defined on a subspace $H$ of $E$, *}
-        txt {* and $h$ is an extension of $f$ that is again bounded by $p$. \skp *}
+        "is_subspace H E" "is_subspace F H" "graph F f \<subseteq> graph H h" 
+        "\<forall>x \<in> H. h x \<le> 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 & 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 \\<le> p x)" by (simp! add: norm_pres_extension_D)
+        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 \<le> p x)" by (simp! add: norm_pres_extension_D)
         thus ?thesis by (elim exE conjE) rule
       qed
       have h: "is_vectorspace H" ..
       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'" 
-          obtain x' where "x' \\<in> E" "x' \\<notin> H" 
-          txt {* Pick $x' \in E \setminus H$. \skp *}
+        have "\<exists>g' \<in> M. g \<subseteq> g' \<and> g \<noteq> g'" 
+          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> \<zero>"
+          have x': "x' \<noteq> 0"
           proof (rule classical)
-            presume "x' = \<zero>"
-            with h have "x' \\<in> H" by simp
+            presume "x' = 0"
+            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 *}
           show ?thesis
-            obtain xi where "\\<forall>y \\<in> H. - p (y + x') - h y \\<le> xi 
-                              \\<and> xi \\<le> p (y + x') - h y" 
-            txt {* Pick a real number $\xi$ that fulfills certain inequations; this will *}
-            txt {* be used to establish that $h'$ is a norm-preserving extension of $h$. \skp *}
+            obtain xi where "\<forall>y \<in> H. - p (y + x') - h y \<le> xi 
+                              \<and> xi \<le> 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 "EX xi. ALL y:H. - p (y + x') - h y <= xi 
-                              & 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:H" "v: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)"
@@ -138,25 +197,25 @@
               thus ?thesis by rule rule
             qed
 
-            def h' == "\\<lambda>x. let (y,a) = \\<epsilon>(y,a). x = y + a \<prod> 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'" 
-              txt {* Show that $h'$ is an extension of $h$ \dots \skp *}
-proof
-		show "g \\<subseteq> 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'"
 		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 \<prod> x' & y \\<in> H)
-                         = (t, #0)" 
-		      by (rule decomp_H0_H [OF _ _ _ _ _ x'])
+		    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)
@@ -167,33 +226,33 @@
 		  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' = \<zero> + x'" by (simp!)
-		      from h show "\<zero> \\<in> H" ..
-		      show "x' \\<in> lin x'" by (rule x_lin_x)
+		      show "x' = 0 + x'" by (simp!)
+		      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" 
-              txt {* and $h'$ is norm-preserving. \skp *} 
+	      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 h0_lf [OF _ _ _ _ _ _ x']) (simp!)+
-		  show "is_subspace H' E"
+		    by (rule h'_lf) (simp! add: x')+
+                  show "is_subspace H' E" 
 		    by (unfold H'_def) (rule vs_sum_subspace [OF _ lin_subspace])
 		  have "is_subspace F H" .
 		  also from h lin_vs 
@@ -201,49 +260,259 @@
 		  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 (*) x' & y \\<in> H)"
-		      by (rule decomp_H0_H [RS sym, OF _ _ _ _ _ x']) (simp!)+
+		      "(x, #0) = (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)"
+		      proof (rule decomp_H'_H [RS sym]) qed (simp! add: x')+
 		    also have 
-		      "(let (y,a) = (SOME (y,a). x = y + a (*) x' & 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 \\<le> p x"
-		    by (rule h0_norm_pres [OF _ _ _ _ x'])
+		  show "\<forall>x \<in> H'. h' x \<le> 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
         qed
-        hence "\\<not>(\\<forall>x \\<in> M. g \\<subseteq> x \\<longrightarrow> 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 \\<le> 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 \<le> 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 (intro ballI, rule sym)
-	  fix x assume "x \\<in> F" show "f x = h x " ..
+	  fix x assume "x \<in> F" show "f x = h x " ..
 	qed
-	from eq show "\\<forall>x \\<in> E. h x \\<le> p x" by (force!)
+	from eq show "\<forall>x \<in> E. h x \<le> p x" by (force!)
       qed
     qed
   qed
-qed text_raw {* \smallskip\\ *}
+qed 
+
+
+
+subsection  {* Alternative formulation *}
+
+text {* The following alternative formulation of the Hahn-Banach
+Theorem\label{abs-HahnBanach} uses the fact that for a real linear form
+$f$ and a seminorm $p$ the
+following inequations are equivalent:\footnote{This was shown in lemma
+$\idt{abs{\dsh}ineq{\dsh}iff}$ (see page \pageref{abs-ineq-iff}).}
+\begin{matharray}{ll}
+\forall x\in H.\ap |h\ap x|\leq p\ap x& {\rm and}\\
+\forall x\in H.\ap h\ap x\leq p\ap x\\
+\end{matharray}
+*}
+
+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)"
+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)"
+    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"
+      by (simp! add: abs_ineq_iff [OF subspace_refl])
+    thus ?thesis by (intro exI conjI)
+  qed
+qed
+
+subsection {* The Hahn-Banach Theorem for normed spaces *}
+
+text {* Every continuous linear form $f$ on a subspace $F$ of a
+norm space $E$, can be extended to a continuous linear form $g$ on
+$E$ such that $\fnorm{f} = \fnorm {g}$. *}
+
+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"
+proof -
+  assume e_norm: "is_normed_vectorspace E norm"
+  assume f: "is_subspace F E" "is_linearform F f"
+  assume f_cont: "is_continuous F norm f"
+  have e: "is_vectorspace E" ..
+  hence f_norm: "is_normed_vectorspace F norm" ..
+
+  txt{* We define a function $p$ on $E$ as follows:
+  \begin{matharray}{l}
+  p \: x = \fnorm f \cdot \norm x\\
+  \end{matharray}
+  *}
+
+  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"
+
+    txt{* $p$ is positive definite: *}
+
+    show "#0 <= p x"
+    proof (unfold p_def, rule real_le_mult_order1a) thm fnorm_ge_zero
+      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"
+    proof - 
+      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" 
+        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)"
+        by (simp! only: real_mult_left_commute)
+      also have "... = |a| * p x" by (simp!)
+      finally show ?thesis .
+    qed
+
+    txt{* Furthermore, $p$ is subadditive: *}
+
+    show "p (x + y) <= p x + p y"
+    proof -
+      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)"
+      proof (rule real_mult_le_le_mono1a)
+        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"
+        by (simp! only: real_add_mult_distrib2)
+      finally show ?thesis by (simp!)
+    qed
+  qed
+
+  txt{* $f$ is bounded by $p$. *} 
+
+  have "\<forall>x \<in> F. |f x| <= p x"
+  proof
+    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
+
+  txt{* Using the fact that $p$ is a seminorm and 
+  $f$ is bounded by $p$ we can apply the Hahn-Banach Theorem 
+  for real vector spaces. 
+  So $f$ can be extended in a norm-preserving way to some function
+  $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)"
+    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"
+
+    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 
+    $g$ is also continuous: *}
+
+      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"
+          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"
+        (is "?L = ?R")
+      proof (rule order_antisym)
+
+        txt{* First we show $\fnorm g \leq \fnorm f$.  The function norm
+        $\fnorm g$ is defined as the smallest $c\in\bbbR$ such that
+        \begin{matharray}{l}
+        \All {x\in E} {|g\ap x| \leq c \cdot \norm x}
+        \end{matharray}
+        Furthermore holds
+        \begin{matharray}{l}
+        \All {x\in E} {|g\ap x| \leq \fnorm f \cdot \norm x}
+        \end{matharray}
+        *}
+ 
+        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"
+            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" ..
+        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"
+        proof
+          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"
+          proof (rule norm_fx_le_norm_f_norm_x)
+            show "x \<in> E" ..
+          qed
+          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" ..
+        qed
+      qed
+    qed
+  qed
+qed
+
 end
\ No newline at end of file
diff -r 78a11a353473 -r 153853af318b src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Sun Jul 16 21:00:32 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Mon Jul 17 13:58:18 2000 +0200
@@ -35,51 +35,51 @@
 \end{matharray} *};
 
 lemma ex_xi: 
-  "[| is_vectorspace F; !! u v. [| u:F; v:F |] ==> a u <= b v |]
-  ==> EX (xi::real). ALL y:F. a y <= xi & 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:F; v: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:F}";
+  let ?S = "{a u :: real | u. u \<in> F}";
 
-  have "EX 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 \<zero> : ?S"; by force;
-    thus "EX X. X : ?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 "EX Y. isUb UNIV ?S Y"; 
+    show "\<exists>Y. isUb UNIV ?S Y"; 
     proof; 
-      show "isUb UNIV ?S (b \<zero>)";
+      show "isUb UNIV ?S (b 0)";
       proof (intro isUbI setleI ballI);
-        show "b \<zero> : UNIV"; ..;
+        show "b 0 \<in> UNIV"; ..;
       next;
 
         txt {* Every element $y\in S$ is less than $b\ap \zero$: *};
 
-        fix y; assume y: "y : ?S"; 
-        from y; have "EX u:F. y = a u"; by fast;
-        thus "y <= b \<zero>"; 
+        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:F"; 
+          fix u; assume "u \<in> F"; 
           assume "y = a u";
-          also; have "a u <= b \<zero>"; by (rule r) (simp!)+;
+          also; have "a u <= b 0"; by (rule r) (simp!)+;
           finally; show ?thesis; .;
         qed;
       qed;
     qed;
   qed;
 
-  thus "EX xi. ALL y:F. a y <= xi & 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: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:F";
+      fix y; assume "y \<in> F";
       show "xi <= b y";  
       proof (intro isLub_le_isUb isUbI setleI);
-        show "b y : UNIV"; ..;
-        show "ALL ya : ?S. ya <= b y"; 
+        show "b y \<in> UNIV"; ..;
+        show "\<forall>ya \<in> ?S. ya <= b y"; 
         proof;
-          fix au; assume au: "au : ?S ";
-          hence "EX u: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: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;
@@ -120,63 +120,63 @@
 $h_0\ap x = h\ap y + a\cdot \xi$ where $x = y + a\mult \xi$
 is a linear extension of $h$ to $H_0$. *};
 
-lemma h0_lf: 
-  "[| h0 == (\\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<prod> x0 & y:H 
+lemma h'_lf: 
+  "[| h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H 
                 in h y + a * xi);
-  H0 == H + lin x0; is_subspace H E; is_linearform H h; x0 ~: H; 
-  x0 : E; x0 ~= \<zero>; is_vectorspace E |]
-  ==> is_linearform H0 h0";
+  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 h0_def: 
-    "h0 == (\\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<prod> x0 & y:H 
+  assume h'_def: 
+    "h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H 
                in h y + a * xi)"
-    and H0_def: "H0 == H + lin x0" 
-    and vs: "is_subspace H E" "is_linearform H h" "x0 ~: H"
-      "x0 ~= \<zero>" "x0 : E" "is_vectorspace E";
+    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";
 
-  have h0: "is_vectorspace H0"; 
-  proof (unfold H0_def, rule vs_sum_vs);
+  have h': "is_vectorspace H'"; 
+  proof (unfold H'_def, rule vs_sum_vs);
     show "is_subspace (lin x0) E"; ..;
   qed; 
 
   show ?thesis;
   proof;
-    fix x1 x2; assume x1: "x1 : H0" and x2: "x2 : H0"; 
+    fix x1 x2; assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'"; 
 
     txt{* We now have to show that $h_0$ is additive, i.~e.\
     $h_0 \ap (x_1\plus x_2) = h_0\ap x_1 + h_0\ap x_2$
     for $x_1, x_2\in H$. *}; 
 
-    have x1x2: "x1 + x2 : H0"; 
-      by (rule vs_add_closed, rule h0); 
+    have x1x2: "x1 + x2 \<in> H'"; 
+      by (rule vs_add_closed, rule h'); 
     from x1; 
-    have ex_x1: "EX y1 a1. x1 = y1 + a1 \<prod> x0  & y1 : H"; 
-      by (unfold H0_def vs_sum_def lin_def) fast;
+    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: "EX y2 a2. x2 = y2 + a2 \<prod> x0 & y2 : H"; 
-      by (unfold H0_def vs_sum_def lin_def) fast;
+    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: "EX y a. x1 + x2 = y + a \<prod> x0 & y : H";
-      by (unfold H0_def vs_sum_def lin_def) fast;
+    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 "h0 (x1 + x2) = h0 x1 + h0 x2";
+    show "h' (x1 + x2) = h' x1 + h' x2";
     proof (elim exE conjE);
       fix y1 y2 y a1 a2 a;
-      assume y1: "x1 = y1 + a1 \<prod> x0"     and y1': "y1 : H"
-         and y2: "x2 = y2 + a2 \<prod> x0"     and y2': "y2 : H" 
-         and y: "x1 + x2 = y + a \<prod> x0"   and y':  "y  : 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"; 
 
-      have ya: "y1 + y2 = y & a1 + a2 = a"; 
-      proof (rule decomp_H0);;
-	txt_raw {* \label{decomp-H0-use} *};;
-        show "y1 + y2 + (a1 + a2) \<prod> x0 = y + a \<prod> x0"; 
+      have ya: "y1 + y2 = y \<and> a1 + a2 = a"; 
+      proof (rule decomp_H');;
+	txt_raw {* \label{decomp-H-use} *};;
+        show "y1 + y2 + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0"; 
           by (simp! add: vs_add_mult_distrib2 [of E]);
-        show "y1 + y2 : H"; ..;
+        show "y1 + y2 \<in> H"; ..;
       qed;
 
-      have "h0 (x1 + x2) = h y + a * xi";
-	by (rule h0_definite);
+      have "h' (x1 + x2) = h y + a * xi";
+	by (rule h'_definite);
       also; have "... = h (y1 + y2) + (a1 + a2) * xi"; 
         by (simp add: ya);
       also; from vs y1' y2'; 
@@ -185,10 +185,10 @@
                       real_add_mult_distrib);
       also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)"; 
         by simp;
-      also; have "h y1 + a1 * xi = h0 x1"; 
-        by (rule h0_definite [RS sym]);
-      also; have "h y2 + a2 * xi = h0 x2"; 
-        by (rule h0_definite [RS sym]);
+      also; have "h y1 + a1 * xi = h' x1"; 
+        by (rule h'_definite [RS sym]);
+      also; have "h y2 + a2 * xi = h' x2"; 
+        by (rule h'_definite [RS sym]);
       finally; show ?thesis; .;
     qed;
  
@@ -198,39 +198,39 @@
     *}; 
 
   next;  
-    fix c x1; assume x1: "x1 : H0";    
-    have ax1: "c \<prod> x1 : H0";
-      by (rule vs_mult_closed, rule h0);
-    from x1; have ex_x: "!! x. x: H0 
-                        ==> EX y a. x = y + a \<prod> x0 & y : H";
-      by (unfold H0_def vs_sum_def lin_def) fast;
+    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";
+      by (unfold H'_def vs_sum_def lin_def) fast;
 
-    from x1; have ex_x1: "EX y1 a1. x1 = y1 + a1 \<prod> x0 & y1 : H";
-      by (unfold H0_def vs_sum_def lin_def) fast;
-    with ex_x [of "c \<prod> x1", OF ax1];
-    show "h0 (c \<prod> x1) = c * (h0 x1)";  
+    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)";  
     proof (elim exE conjE);
       fix y1 y a1 a; 
-      assume y1: "x1 = y1 + a1 \<prod> x0"       and y1': "y1 : H"
-        and y: "c \<prod> x1 = y  + a  \<prod> x0"   and y':  "y  : 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 \<prod> y1 = y & c * a1 = a"; 
-      proof (rule decomp_H0); 
-	show "c \<prod> y1 + (c * a1) \<prod> x0 = y + a \<prod> x0"; 
-          by (simp! add: add: vs_add_mult_distrib1);
-        show "c \<prod> y1 : H"; ..;
+      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"; 
+          by (simp! add: vs_add_mult_distrib1);
+        show "c \<cdot> y1 \<in> H"; ..;
       qed;
 
-      have "h0 (c \<prod> x1) = h y + a * xi"; 
-	by (rule h0_definite);
-      also; have "... = h (c \<prod> y1) + (c * a1) * xi";
+      have "h' (c \<cdot> x1) = h y + a * xi"; 
+	by (rule h'_definite);
+      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]);
       also; from vs y1'; have "... = c * (h y1 + a1 * xi)"; 
 	by (simp add: real_add_mult_distrib2 real_mult_assoc);
-      also; have "h y1 + a1 * xi = h0 x1"; 
-        by (rule h0_definite [RS sym]);
+      also; have "h y1 + a1 * xi = h' x1"; 
+        by (rule h'_definite [RS sym]);
       finally; show ?thesis; .;
     qed;
   qed;
@@ -239,40 +239,40 @@
 text{* \medskip The linear extension $h_0$ of $h$
 is bounded by the seminorm $p$. *};
 
-lemma h0_norm_pres:
-  "[| h0 == (\\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<prod> x0 & y:H 
+lemma h'_norm_pres:
+  "[| h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H 
                 in h y + a * xi);
-  H0 == H + lin x0; x0 ~: H; x0 : E; x0 ~= \<zero>; is_vectorspace E; 
-  is_subspace H E; is_seminorm E p; is_linearform H h; ALL y:H. h y <= p y; 
-  ALL y:H. - p (y + x0) - h y <= xi & xi <= p (y + x0) - h y |]
-   ==> ALL x:H0. h0 x <= p x"; 
+  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"; 
 proof; 
-  assume h0_def: 
-    "h0 == (\\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<prod> x0 & y:H 
+  assume h'_def: 
+    "h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H 
                in (h y) + a * xi)"
-    and H0_def: "H0 == H + lin x0" 
-    and vs: "x0 ~: H" "x0 : E" "x0 ~= \<zero>" "is_vectorspace E" 
+    and H'_def: "H' == H + lin x0" 
+    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: "ALL y:H. h y <= p y";
-  presume a1: "ALL ya:H. - p (ya + x0) - h ya <= xi";
-  presume a2: "ALL ya:H. xi <= p (ya + x0) - h ya";
-  fix x; assume "x : H0"; 
+    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 : H0 ==> EX y a. x = y + a \<prod> x0 & y : H";
-    by (unfold H0_def vs_sum_def lin_def) fast;
-  have "EX y a. x = y + a \<prod> x0 & y : 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";
     by (rule ex_x);
-  thus "h0 x <= p x";
+  thus "h' x <= p x";
   proof (elim exE conjE);
-    fix y a; assume x: "x = y + a \<prod> x0" and y: "y : H";
-    have "h0 x = h y + a * xi";
-      by (rule h0_definite);
+    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);
 
     txt{* Now we show  
     $h\ap y + a \cdot \xi\leq  p\ap (y\plus a \mult x_0)$ 
     by case analysis on $a$. \label{linorder_linear_split}*};
 
-    also; have "... <= p (y + a \<prod> x0)";
+    also; have "... <= p (y + a \<cdot> x0)";
     proof (rule linorder_linear_split); 
 
       assume z: "a = #0"; 
@@ -282,29 +282,29 @@
     taken as $y/a$: *};
 
     next;
-      assume lz: "a < #0"; hence nz: "a ~= #0"; by simp;
+      assume lz: "a < #0"; hence nz: "a \<noteq> #0"; by simp;
       from a1; 
-      have "- p (rinv a \<prod> y + x0) - h (rinv a \<prod> 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 \<prod> y + x0) - h (rinv a \<prod> y))";
+            <= 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 \<prod> y + x0)) 
-                        - a * (h (rinv a \<prod> y))";
+      also; 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 \<prod> y + x0)) 
-                               = p (a \<prod> (rinv a \<prod> y + x0))";
+      also; from lz vs y; 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 \<prod> 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 \<prod> 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 \<prod> x0) - h y"; .;
+      finally; have "a * xi <= p (y + a \<cdot> x0) - h y"; .;
 
-      hence "h y + a * xi <= h y + p (y + a \<prod> 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;
 
@@ -312,32 +312,32 @@
       taken as $y/a$: *};
 
     next; 
-      assume gz: "#0 < a"; hence nz: "a ~= #0"; by simp;
+      assume gz: "#0 < a"; hence nz: "a \<noteq> #0"; by simp;
       from a2;
-      have "xi <= p (rinv a \<prod> y + x0) - h (rinv a \<prod> y)";
+      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 \<prod> y + x0) - h (rinv a \<prod> y))";
+            <= 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 \<prod> y + x0) 
-                        - a * h (rinv a \<prod> 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 \<prod> y + x0) 
-           = p (a \<prod> (rinv a \<prod> 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 \<prod> x0)";
+      have "... = p (y + a \<cdot> x0)";
         by (simp add: vs_add_mult_distrib1);
-      also; from nz vs y; have "a * h (rinv a \<prod> 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 \<prod> x0) - h y"; .;
+      finally; have "a * xi <= p (y + a \<cdot> x0) - h y"; .;
  
-      hence "h y + a * xi <= h y + (p (y + a \<prod> 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;
@@ -346,4 +346,4 @@
   qed;
 qed blast+; 
 
-end;
\ No newline at end of file
+end;
diff -r 78a11a353473 -r 153853af318b src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Sun Jul 16 21:00:32 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Mon Jul 17 13:58:18 2000 +0200
@@ -7,8 +7,6 @@
 
 theory HahnBanachSupLemmas = FunctionNorm + ZornLemma:
 
-
-
 text{* This section contains some lemmas that will be used in the
 proof of the Hahn-Banach Theorem.
 In this section the following context is presumed. 
@@ -20,7 +18,6 @@
 i.e.\ the supremum of the chain $c$.
 *} 
 
-
 text{* Let $c$ be a chain of norm-preserving extensions of the 
 function $f$ and let $\idt{graph}\ap H\ap h$ be the supremum of $c$. 
 Every element in $H$ is member of
@@ -28,38 +25,38 @@
 
 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 & (x, h x) \<in> graph H' h' 
-       & 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 \\<le> p x)"
+  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 \<le> 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"
+     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" 
+  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" ..
+    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 
-                  & 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 \\<le> p x)"
+    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 \<le> 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 \\<le> p x"
+        "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x"
       show ?thesis 
       proof (intro exI conjI)
         show "graph H' h' \<in> c" by (simp!)
@@ -78,28 +75,28 @@
 
 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' & graph H' h' \\<subseteq> graph H h 
-      & 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 \\<le> p x)" 
+  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 \<le> 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"  
+     and u: "graph H h = \<Union> c" "x \<in> H"  
 
-  have "\<exists> H' h'. graph H' h' \<in> c & (x, h x) \<in> graph H' h' 
-       & 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 \\<le> 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 \<le> 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"
       "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 \\<le> p x"
+      "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> 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
@@ -111,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' & y\<in>H' & graph H' h' \\<subseteq> graph H h 
-      & 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 \\<le> 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 \<le> 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 & (x, h x) \<in> graph H' h'
-       & 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 \\<le> 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 \<le> 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 & (y, h y) \<in> graph H'' h''
-       & 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 \\<le> 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 \<le> 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 \\<le> p x"
+      "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> 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 \\<le> p x"
+      "graph F f \<subseteq> graph H'' h''" "\<forall>x \<in> H''. h'' x \<le> 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
@@ -161,23 +158,23 @@
       show ?thesis
       proof (intro exI conjI)
         have "(x, h x) \<in> graph H'' h''" .
-        also have "... \\<subseteq> graph H' h'" .
-        finally have xh\<in> "(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"
+        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''" ..
+        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"
+        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,14 +184,14 @@
 
 
 text{* \medskip The relation induced by the graph of the supremum
-of a chain $c$ is definite, i.~e.~it is the graph of a function. *}
+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"
+  (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)
 
@@ -203,7 +200,7 @@
     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"  
@@ -219,7 +216,7 @@
       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
@@ -247,27 +244,27 @@
 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' & y\<in>H' & graph H' h' \\<subseteq> graph H h 
-            & 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 \\<le> p x)"
+    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 \<le> 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)
@@ -279,24 +276,24 @@
     qed
   next  
     fix a x assume "x \<in> H"
-    have "\<exists> H' h'. x\<in>H' & graph H' h' \\<subseteq> graph H h 
-            & 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 \\<le> p x)"
+    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 \<le> p x)"
       by (rule some_H'h')
 
     txt{* We have to show that $h$ is multiplicative. *}
 
-    thus "h (a \<prod> 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 \<prod> 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 \<prod> x \<in> H'" ..
-      with b have "h' (a \<prod> x) = h (a \<prod> x)" ..
+      also have "a \<cdot> x \<in> H'" ..
+      with b have "h' (a \<cdot> x) = h (a \<cdot> x)" ..
       finally show ?thesis .
     qed
   qed
@@ -309,34 +306,34 @@
 for every element of the chain.*}
 
 lemma sup_ext:
-  "[| M = norm_pres_extensions E p F f; c\<in> chain M; \<exists> x. x\<in>c; 
-  graph H h = Union 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" ..
+    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
-             & is_linearform G g 
-             & is_subspace G E
-             & is_subspace F G
-             & graph F f \\<subseteq> graph G g 
-             & (\<forall> x\<in>G. g x \\<le> 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 \<le> 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" .
+      hence "x \<subseteq> \<Union> c" by fast
+      also have [RS sym]: "graph H h = \<Union> c" .
       finally show ?thesis .
     qed
   qed
@@ -348,30 +345,30 @@
 vector space. *}
 
 lemma sup_supF: 
-  "[| 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 |] 
+  "[|  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 "\<zero> \<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"
+      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 \<prod> 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 \<prod> x \<in> F" by (simp!)
+      show "a \<cdot> x \<in> F" by (simp!)
     qed
   qed
 qed
@@ -380,78 +377,78 @@
 of $E$. *}
 
 lemma sup_subE: 
-  "[| 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 |] 
+  "[| 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 "\<zero> \<in> F" ..
+    have "0 \<in> F" ..
     also have "is_subspace F H" by (rule sup_supF) 
-    hence "F \\<subseteq> H" ..
-    finally show "\<zero> \<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' & graph H' h' \\<subseteq> graph H h
-              & 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 \\<le> 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 \<le> 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' & y\<in>H' & graph H' h' \\<subseteq> graph H h 
-              & 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 \\<le> 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 \<le> p x)" 
 	by (rule some_H'h'2) 
       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"
+        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" ..
+	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 \<prod> 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' & graph H' h' \\<subseteq> graph H h
-              & 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 \\<le> 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 \<le> p x)" 
 	by (rule some_H'h') 
-      thus "a \<prod> 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 \<prod> 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
@@ -463,24 +460,24 @@
 bounded by $p$.
 *}
 
-lemma sup_norm_pres\<in> 
-  "[| M = norm_pres_extensions E p F f; c\<in> chain M; 
-  graph H h = Union c |] ==> \<forall> x\<in>H. h x \\<le> p x"
+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 \<le> 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' & graph H' h' \\<subseteq> graph H h 
-          & 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 \\<le> 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 \<le> p x)" 
     by (rule some_H'h')
-  thus "h x \\<le> p x" 
+  thus "h x \<le> 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 \\<le> p x"
+    assume "x \<in> H'" "graph H' h' \<subseteq> graph H h" 
+      and a: "\<forall>x \<in> H'. h' x \<le> p x"
     have [RS sym]: "h' x = h x" ..
-    also from a have "h' x \\<le> p x " ..
+    also from a have "h' x \<le> p x " ..
     finally show ?thesis .  
   qed
 qed
@@ -499,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. abs (h x) \\<le> p x) = (\<forall> x\<in>H. h x \\<le> p x)" 
+  ==> (\<forall>x \<in> H. |h x| \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)" 
   (concl is "?L = ?R")
 proof -
   assume "is_subspace H E" "is_vectorspace E" "is_seminorm E p" 
@@ -510,28 +507,28 @@
     assume l: ?L
     show ?R
     proof
-      fix x assume x: "x\<in>H"
-      have "h x \\<le> abs (h x)" by (rule abs_ge_self)
-      also from l have "... \\<le> p x" ..
-      finally show "h x \\<le> p x" .
+      fix x assume x: "x \<in> H"
+      have "h x \<le> |h x|" by (rule abs_ge_self)
+      also from l have "... \<le> p x" ..
+      finally show "h x \<le> p x" .
     qed
   next
     assume r: ?R
     show ?L
     proof 
-      fix x assume "x\<in>H"
-      show "!! a b \<in>: real. [| - a \\<le> b; b \\<le> a |] ==> abs b \\<le> a"
+      fix x assume "x \<in> H"
+      show "!! a b :: real. [| - a \<le> b; b \<le> a |] ==> |b| \<le> a"
         by arith
-      show "- p x \\<le> h x"
+      show "- p x \<le> h x"
       proof (rule real_minus_le)
 	from h have "- h x = h (- x)" 
           by (rule linearform_neg [RS sym])
-	also from r have "... \\<le> p (- x)" by (simp!)
+	also from r have "... \<le> p (- x)" by (simp!)
 	also have "... = p x" 
           by (rule seminorm_minus [OF _ subspace_subsetD])
-	finally show "- h x \\<le> p x" . 
+	finally show "- h x \<le> p x" . 
       qed
-      from r show "h x \\<le> p x" .. 
+      from r show "h x \<le> p x" .. 
     qed
   qed
 qed  
diff -r 78a11a353473 -r 153853af318b src/HOL/Real/HahnBanach/Linearform.thy
--- a/src/HOL/Real/HahnBanach/Linearform.thy	Sun Jul 16 21:00:32 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Linearform.thy	Mon Jul 17 13:58:18 2000 +0200
@@ -11,41 +11,41 @@
 space into the reals that is additive and multiplicative. *}
 
 constdefs
-  is_linearform :: "['a::{minus, plus} set, 'a => real] => bool" 
+  is_linearform :: "['a::{plus, minus, zero} set, 'a => real] => bool" 
   "is_linearform V f == 
-      (ALL x: V. ALL y: V. f (x + y) = f x + f y) &
-      (ALL x: V. ALL a. f (a (*) x) = a * (f x))" 
+      (\<forall>x \<in> V. \<forall>y \<in> V. f (x + y) = f x + f y) \<and>
+      (\<forall>x \<in> V. \<forall>a. f (a \<cdot> x) = a * (f x))" 
 
 lemma is_linearformI [intro]: 
-  "[| !! x y. [| x : V; y : V |] ==> f (x + y) = f x + f y;
-    !! x c. x : V ==> f (c (*) x) = c * f x |]
+  "[| !! x y. [| x \<in> V; y \<in> V |] ==> f (x + y) = f x + f y;
+    !! x c. x \<in> V ==> f (c \<cdot> x) = c * f x |]
  ==> is_linearform V f"
  by (unfold is_linearform_def) force
 
 lemma linearform_add [intro??]: 
-  "[| is_linearform V f; x:V; y:V |] ==> f (x + y) = f x + f y"
+  "[| is_linearform V f; x \<in> V; y \<in> V |] ==> f (x + y) = f x + f y"
   by (unfold is_linearform_def) fast
 
 lemma linearform_mult [intro??]: 
-  "[| is_linearform V f; x:V |] ==>  f (a (*) x) = a * (f x)" 
+  "[| is_linearform V f; x \<in> V |] ==>  f (a \<cdot> x) = a * (f x)" 
   by (unfold is_linearform_def) fast
 
 lemma linearform_neg [intro??]:
-  "[|  is_vectorspace V; is_linearform V f; x:V|] 
+  "[|  is_vectorspace V; is_linearform V f; x \<in> V|] 
   ==> f (- x) = - f x"
 proof - 
-  assume "is_linearform V f" "is_vectorspace V" "x:V"
-  have "f (- x) = f ((- #1) (*) x)" by (simp! add: negate_eq1)
+  assume "is_linearform V f" "is_vectorspace V" "x \<in> V"
+  have "f (- x) = f ((- #1) \<cdot> x)" by (simp! add: negate_eq1)
   also have "... = (- #1) * (f x)" by (rule linearform_mult)
   also have "... = - (f x)" by (simp!)
   finally show ?thesis .
 qed
 
 lemma linearform_diff [intro??]: 
-  "[| is_vectorspace V; is_linearform V f; x:V; y:V |] 
+  "[| is_vectorspace V; is_linearform V f; x \<in> V; y \<in> V |] 
   ==> f (x - y) = f x - f y"  
 proof -
-  assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V"
+  assume "is_vectorspace V" "is_linearform V f" "x \<in> V" "y \<in> V"
   have "f (x - y) = f (x + - y)" by (simp! only: diff_eq1)
   also have "... = f x + f (- y)" 
     by (rule linearform_add) (simp!)+
@@ -56,14 +56,14 @@
 text{* Every linear form yields $0$ for the $\zero$ vector.*}
 
 lemma linearform_zero [intro??, simp]: 
-  "[| is_vectorspace V; is_linearform V f |] ==> f 00 = #0" 
+  "[| is_vectorspace V; is_linearform V f |] ==> f 0 = #0"
 proof - 
   assume "is_vectorspace V" "is_linearform V f"
-  have "f 00 = f (00 - 00)" by (simp!)
-  also have "... = f 00 - f 00" 
+  have "f 0 = f (0 - 0)" by (simp!)
+  also have "... = f 0 - f 0" 
     by (rule linearform_diff) (simp!)+
   also have "... = #0" by simp
-  finally show "f 00 = #0" .
+  finally show "f 0 = #0" .
 qed 
 
 end
\ No newline at end of file
diff -r 78a11a353473 -r 153853af318b src/HOL/Real/HahnBanach/NormedSpace.thy
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Sun Jul 16 21:00:32 2000 +0200
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Mon Jul 17 13:58:18 2000 +0200
@@ -7,6 +7,8 @@
 
 theory NormedSpace =  Subspace:
 
+syntax 
+  abs :: "real \<Rightarrow> real" ("|_|")
 
 subsection {* Quasinorms *}
 
@@ -15,57 +17,57 @@
 definite, absolute homogenous and subadditive.  *}
 
 constdefs
-  is_seminorm :: "['a::{plus, minus} set, 'a => real] => bool"
-  "is_seminorm V norm == ALL x: V. ALL y:V. ALL a. 
+  is_seminorm :: "['a::{plus, minus, zero} set, 'a => real] => bool"
+  "is_seminorm V norm == \<forall>x \<in>  V. \<forall>y \<in> V. \<forall>a. 
         #0 <= norm x 
-      & norm (a (*) x) = (abs a) * (norm x)
-      & norm (x + y) <= norm x + norm y"
+      \<and> norm (a \<cdot> x) = |a| * norm x
+      \<and> norm (x + y) <= norm x + norm y"
 
 lemma is_seminormI [intro]: 
-  "[| !! x y a. [| x:V; y:V|] ==> #0 <= norm x;
-  !! x a. x:V ==> norm (a (*) x) = (abs a) * (norm x);
-  !! x y. [|x:V; y:V |] ==> norm (x + y) <= norm x + norm y |] 
+  "[| !! x y a. [| x \<in> V; y \<in> V|] ==> #0 <= norm x;
+  !! x a. x \<in> V ==> norm (a \<cdot> x) = |a| * norm x;
+  !! x y. [|x \<in> V; y \<in> V |] ==> norm (x + y) <= norm x + norm y |] 
   ==> is_seminorm V norm"
   by (unfold is_seminorm_def, force)
 
 lemma seminorm_ge_zero [intro??]:
-  "[| is_seminorm V norm; x:V |] ==> #0 <= norm x"
+  "[| is_seminorm V norm; x \<in> V |] ==> #0 <= norm x"
   by (unfold is_seminorm_def, force)
 
 lemma seminorm_abs_homogenous: 
-  "[| is_seminorm V norm; x:V |] 
-  ==> norm (a (*) x) = (abs a) * (norm x)"
+  "[| is_seminorm V norm; x \<in> V |] 
+  ==> norm (a \<cdot> x) = |a| * norm x"
   by (unfold is_seminorm_def, force)
 
 lemma seminorm_subadditive: 
-  "[| is_seminorm V norm; x:V; y:V |] 
+  "[| is_seminorm V norm; x \<in> V; y \<in> V |] 
   ==> norm (x + y) <= norm x + norm y"
   by (unfold is_seminorm_def, force)
 
 lemma seminorm_diff_subadditive: 
-  "[| is_seminorm V norm; x:V; y:V; is_vectorspace V |] 
+  "[| is_seminorm V norm; x \<in> V; y \<in> V; is_vectorspace V |] 
   ==> norm (x - y) <= norm x + norm y"
 proof -
-  assume "is_seminorm V norm" "x:V" "y:V" "is_vectorspace V"
-  have "norm (x - y) = norm (x + - #1 (*) y)"  
+  assume "is_seminorm V norm" "x \<in> V" "y \<in> V" "is_vectorspace V"
+  have "norm (x - y) = norm (x + - #1 \<cdot> y)"  
     by (simp! add: diff_eq2 negate_eq2a)
-  also have "... <= norm x + norm  (- #1 (*) y)" 
+  also have "... <= norm x + norm  (- #1 \<cdot> y)" 
     by (simp! add: seminorm_subadditive)
-  also have "norm (- #1 (*) y) = abs (- #1) * norm y" 
+  also have "norm (- #1 \<cdot> y) = |- #1| * norm y" 
     by (rule seminorm_abs_homogenous)
-  also have "abs (- #1) = (#1::real)" by (rule abs_minus_one)
+  also have "|- #1| = (#1::real)" by (rule abs_minus_one)
   finally show "norm (x - y) <= norm x + norm y" by simp
 qed
 
 lemma seminorm_minus: 
-  "[| is_seminorm V norm; x:V; is_vectorspace V |] 
+  "[| is_seminorm V norm; x \<in> V; is_vectorspace V |] 
   ==> norm (- x) = norm x"
 proof -
-  assume "is_seminorm V norm" "x:V" "is_vectorspace V"
-  have "norm (- x) = norm (- #1 (*) x)" by (simp! only: negate_eq1)
-  also have "... = abs (- #1) * norm x" 
+  assume "is_seminorm V norm" "x \<in> V" "is_vectorspace V"
+  have "norm (- x) = norm (- #1 \<cdot> x)" by (simp! only: negate_eq1)
+  also have "... = |- #1| * norm x" 
     by (rule seminorm_abs_homogenous)
-  also have "abs (- #1) = (#1::real)" by (rule abs_minus_one)
+  also have "|- #1| = (#1::real)" by (rule abs_minus_one)
   finally show "norm (- x) = norm x" by simp
 qed
 
@@ -76,24 +78,24 @@
 $\zero$ vector to $0$. *}
 
 constdefs
-  is_norm :: "['a::{minus, plus} set, 'a => real] => bool"
-  "is_norm V norm == ALL x: V.  is_seminorm V norm 
-      & (norm x = #0) = (x = 00)"
+  is_norm :: "['a::{plus, minus, zero} set, 'a => real] => bool"
+  "is_norm V norm == \<forall>x \<in> V.  is_seminorm V norm 
+      \<and> (norm x = #0) = (x = 0)"
 
 lemma is_normI [intro]: 
-  "ALL x: V.  is_seminorm V norm  & (norm x = #0) = (x = 00) 
+  "\<forall>x \<in> V.  is_seminorm V norm  \<and> (norm x = #0) = (x = 0) 
   ==> is_norm V norm" by (simp only: is_norm_def)
 
 lemma norm_is_seminorm [intro??]: 
-  "[| is_norm V norm; x:V |] ==> is_seminorm V norm"
+  "[| is_norm V norm; x \<in> V |] ==> is_seminorm V norm"
   by (unfold is_norm_def, force)
 
 lemma norm_zero_iff: 
-  "[| is_norm V norm; x:V |] ==> (norm x = #0) = (x = 00)"
+  "[| is_norm V norm; x \<in> V |] ==> (norm x = #0) = (x = 0)"
   by (unfold is_norm_def, force)
 
 lemma norm_ge_zero [intro??]:
-  "[|is_norm V norm; x:V |] ==> #0 <= norm x"
+  "[|is_norm V norm; x \<in> V |] ==> #0 <= norm x"
   by (unfold is_norm_def is_seminorm_def, force)
 
 
@@ -104,10 +106,9 @@
 
 constdefs
   is_normed_vectorspace :: 
-  "['a::{plus, minus} set, 'a => real] => bool"
+  "['a::{plus, minus, zero} set, 'a => real] => bool"
   "is_normed_vectorspace V norm ==
-      is_vectorspace V &
-      is_norm V norm"
+      is_vectorspace V \<and> is_norm V norm"
 
 lemma normed_vsI [intro]: 
   "[| is_vectorspace V; is_norm V norm |] 
@@ -123,32 +124,32 @@
   by (unfold is_normed_vectorspace_def, elim conjE)
 
 lemma normed_vs_norm_ge_zero [intro??]: 
-  "[| is_normed_vectorspace V norm; x:V |] ==> #0 <= norm x"
+  "[| is_normed_vectorspace V norm; x \<in> V |] ==> #0 <= norm x"
   by (unfold is_normed_vectorspace_def, rule, elim conjE)
 
 lemma normed_vs_norm_gt_zero [intro??]: 
-  "[| is_normed_vectorspace V norm; x:V; x ~= 00 |] ==> #0 < norm x"
+  "[| is_normed_vectorspace V norm; x \<in> V; x \<noteq> 0 |] ==> #0 < norm x"
 proof (unfold is_normed_vectorspace_def, elim conjE)
-  assume "x : V" "x ~= 00" "is_vectorspace V" "is_norm V norm"
+  assume "x \<in> V" "x \<noteq> 0" "is_vectorspace V" "is_norm V norm"
   have "#0 <= norm x" ..
-  also have "#0 ~= norm x"
+  also have "#0 \<noteq> norm x"
   proof
     presume "norm x = #0"
-    also have "?this = (x = 00)" by (rule norm_zero_iff)
-    finally have "x = 00" .
+    also have "?this = (x = 0)" by (rule norm_zero_iff)
+    finally have "x = 0" .
     thus "False" by contradiction
   qed (rule sym)
   finally show "#0 < norm x" .
 qed
 
 lemma normed_vs_norm_abs_homogenous [intro??]: 
-  "[| is_normed_vectorspace V norm; x:V |] 
-  ==> norm (a (*) x) = (abs a) * (norm x)"
+  "[| is_normed_vectorspace V norm; x \<in> V |] 
+  ==> norm (a \<cdot> x) = |a| * norm x"
   by (rule seminorm_abs_homogenous, rule norm_is_seminorm, 
       rule normed_vs_norm)
 
 lemma normed_vs_norm_subadditive [intro??]: 
-  "[| is_normed_vectorspace V norm; x:V; y:V |] 
+  "[| is_normed_vectorspace V norm; x \<in> V; y \<in> V |] 
   ==> norm (x + y) <= norm x + norm y"
   by (rule seminorm_subadditive, rule norm_is_seminorm, 
      rule normed_vs_norm)
@@ -157,7 +158,7 @@
 normed vectorspace.*}
 
 lemma subspace_normed_vs [intro??]: 
-  "[| is_subspace F E; is_vectorspace E; 
+  "[| is_vectorspace E; is_subspace F E;
   is_normed_vectorspace E norm |] ==> is_normed_vectorspace F norm"
 proof (rule normed_vsI)
   assume "is_subspace F E" "is_vectorspace E" 
@@ -167,15 +168,15 @@
   proof (intro is_normI ballI conjI)
     show "is_seminorm F norm" 
     proof
-      fix x y a presume "x : E"
+      fix x y a presume "x \<in> E"
       show "#0 <= norm x" ..
-      show "norm (a (*) x) = abs a * norm x" ..
-      presume "y : E"
+      show "norm (a \<cdot> x) = |a| * norm x" ..
+      presume "y \<in> E"
       show "norm (x + y) <= norm x + norm y" ..
     qed (simp!)+
 
-    fix x assume "x : F"
-    show "(norm x = #0) = (x = 00)" 
+    fix x assume "x \<in> F"
+    show "(norm x = #0) = (x = 0)" 
     proof (rule norm_zero_iff)
       show "is_norm E norm" ..
     qed (simp!)
diff -r 78a11a353473 -r 153853af318b src/HOL/Real/HahnBanach/Subspace.thy
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Sun Jul 16 21:00:32 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Mon Jul 17 13:58:18 2000 +0200
@@ -16,39 +16,39 @@
 scalar multiplication. *}
 
 constdefs 
-  is_subspace ::  "['a::{minus, plus} set, 'a set] => bool"
-  "is_subspace U V == U ~= {} & U <= V 
-     & (ALL x:U. ALL y:U. ALL a. x + y : U & a (*) x : U)"
+  is_subspace ::  "['a::{plus, minus, zero} set, 'a set] => bool"
+  "is_subspace U V == U \<noteq> {} \<and> U <= V 
+     \<and> (\<forall>x \<in> U. \<forall>y \<in> U. \<forall>a. x + y \<in> U \<and> a \<cdot> x\<in> U)"
 
 lemma subspaceI [intro]: 
-  "[| 00 : U; U <= V; ALL x:U. ALL y:U. (x + y : U); 
-  ALL x:U. ALL a. a (*) x : U |]
+  "[| 0 \<in> U; U <= V; \<forall>x \<in> U. \<forall>y \<in> U. (x + y \<in> U); 
+  \<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U |]
   ==> is_subspace U V"
 proof (unfold is_subspace_def, intro conjI) 
-  assume "00 : U" thus "U ~= {}" by fast
+  assume "0 \<in> U" thus "U \<noteq> {}" by fast
 qed (simp+)
 
-lemma subspace_not_empty [intro??]: "is_subspace U V ==> U ~= {}"
+lemma subspace_not_empty [intro??]: "is_subspace U V ==> U \<noteq> {}"
   by (unfold is_subspace_def) simp 
 
 lemma subspace_subset [intro??]: "is_subspace U V ==> U <= V"
   by (unfold is_subspace_def) simp
 
 lemma subspace_subsetD [simp, intro??]: 
-  "[| is_subspace U V; x:U |] ==> x:V"
+  "[| is_subspace U V; x \<in> U |] ==> x \<in> V"
   by (unfold is_subspace_def) force
 
 lemma subspace_add_closed [simp, intro??]: 
-  "[| is_subspace U V; x:U; y:U |] ==> x + y : U"
+  "[| is_subspace U V; x \<in> U; y \<in> U |] ==> x + y \<in> U"
   by (unfold is_subspace_def) simp
 
 lemma subspace_mult_closed [simp, intro??]: 
-  "[| is_subspace U V; x:U |] ==> a (*) x : U"
+  "[| is_subspace U V; x \<in> U |] ==> a \<cdot> x \<in> U"
   by (unfold is_subspace_def) simp
 
 lemma subspace_diff_closed [simp, intro??]: 
-  "[| is_subspace U V; is_vectorspace V; x:U; y:U |] 
-  ==> x - y : U"
+  "[| is_subspace U V; is_vectorspace V; x \<in> U; y \<in> U |] 
+  ==> x - y \<in> U"
   by (simp! add: diff_eq1 negate_eq1)
 
 text {* Similar as for linear spaces, the existence of the 
@@ -56,23 +56,23 @@
 of the carrier set and by vector space laws.*}
 
 lemma zero_in_subspace [intro??]:
-  "[| is_subspace U V; is_vectorspace V |] ==> 00 : U"
+  "[| is_subspace U V; is_vectorspace V |] ==> 0 \<in> U"
 proof - 
   assume "is_subspace U V" and v: "is_vectorspace V"
-  have "U ~= {}" ..
-  hence "EX x. x:U" by force
+  have "U \<noteq> {}" ..
+  hence "\<exists>x. x \<in> U" by force
   thus ?thesis 
   proof 
-    fix x assume u: "x:U" 
-    hence "x:V" by (simp!)
-    with v have "00 = x - x" by (simp!)
-    also have "... : U" by (rule subspace_diff_closed)
+    fix x assume u: "x \<in> U" 
+    hence "x \<in> V" by (simp!)
+    with v have "0 = x - x" by (simp!)
+    also have "... \<in> U" by (rule subspace_diff_closed)
     finally show ?thesis .
   qed
 qed
 
 lemma subspace_neg_closed [simp, intro??]: 
-  "[| is_subspace U V; is_vectorspace V; x:U |] ==> - x : U"
+  "[| is_subspace U V; is_vectorspace V; x \<in> U |] ==> - x \<in> U"
   by (simp add: negate_eq1)
 
 text_raw {* \medskip *}
@@ -84,11 +84,11 @@
   assume "is_subspace U V" "is_vectorspace V"
   show ?thesis
   proof 
-    show "00 : U" ..
-    show "ALL x:U. ALL a. a (*) x : U" by (simp!)
-    show "ALL x:U. ALL y:U. x + y : U" by (simp!)
-    show "ALL x:U. - x = -#1 (*) x" by (simp! add: negate_eq1)
-    show "ALL x:U. ALL y:U. x - y =  x + - y" 
+    show "0 \<in> U" ..
+    show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U" by (simp!)
+    show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U" by (simp!)
+    show "\<forall>x \<in> U. - x = -#1 \<cdot> x" by (simp! add: negate_eq1)
+    show "\<forall>x \<in> U. \<forall>y \<in> U. x - y =  x + - y" 
       by (simp! add: diff_eq1)
   qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+
 qed
@@ -98,10 +98,10 @@
 lemma subspace_refl [intro]: "is_vectorspace V ==> is_subspace V V"
 proof 
   assume "is_vectorspace V"
-  show "00 : V" ..
+  show "0 \<in> V" ..
   show "V <= V" ..
-  show "ALL x:V. ALL y:V. x + y : V" by (simp!)
-  show "ALL x:V. ALL a. a (*) x : V" by (simp!)
+  show "\<forall>x \<in> V. \<forall>y \<in> V. x + y \<in> V" by (simp!)
+  show "\<forall>x \<in> V. \<forall>a. a \<cdot> x \<in> V" by (simp!)
 qed
 
 text {* The subspace relation is transitive. *}
@@ -111,22 +111,22 @@
   ==> is_subspace U W"
 proof 
   assume "is_subspace U V" "is_subspace V W" "is_vectorspace V"
-  show "00 : U" ..
+  show "0 \<in> U" ..
 
   have "U <= V" ..
   also have "V <= W" ..
   finally show "U <= W" .
 
-  show "ALL x:U. ALL y:U. x + y : U" 
+  show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U" 
   proof (intro ballI)
-    fix x y assume "x:U" "y:U"
-    show "x + y : U" by (simp!)
+    fix x y assume "x \<in> U" "y \<in> U"
+    show "x + y \<in> U" by (simp!)
   qed
 
-  show "ALL x:U. ALL a. a (*) x : U"
+  show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U"
   proof (intro ballI allI)
-    fix x a assume "x:U"
-    show "a (*) x : U" by (simp!)
+    fix x a assume "x \<in> U"
+    show "a \<cdot> x \<in> U" by (simp!)
   qed
 qed
 
@@ -138,60 +138,60 @@
 scalar multiples of $x$. *}
 
 constdefs
-  lin :: "'a => 'a set"
-  "lin x == {a (*) x | a. True}" 
+  lin :: "('a::{minus,plus,zero}) => 'a set"
+  "lin x == {a \<cdot> x | a. True}" 
 
-lemma linD: "x : lin v = (EX a::real. x = a (*) v)"
+lemma linD: "x \<in> lin v = (\<exists>a::real. x = a \<cdot> v)"
   by (unfold lin_def) fast
 
-lemma linI [intro??]: "a (*) x0 : lin x0"
+lemma linI [intro??]: "a \<cdot> x0 \<in> lin x0"
   by (unfold lin_def) fast
 
 text {* Every vector is contained in its linear closure. *}
 
-lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x : lin x"
+lemma x_lin_x: "[| is_vectorspace V; x \<in> V |] ==> x \<in> lin x"
 proof (unfold lin_def, intro CollectI exI conjI)
-  assume "is_vectorspace V" "x:V"
-  show "x = #1 (*) x" by (simp!)
+  assume "is_vectorspace V" "x \<in> V"
+  show "x = #1 \<cdot> x" by (simp!)
 qed simp
 
 text {* Any linear closure is a subspace. *}
 
 lemma lin_subspace [intro??]: 
-  "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V"
+  "[| is_vectorspace V; x \<in> V |] ==> is_subspace (lin x) V"
 proof
-  assume "is_vectorspace V" "x:V"
-  show "00 : lin x" 
+  assume "is_vectorspace V" "x \<in> V"
+  show "0 \<in> lin x" 
   proof (unfold lin_def, intro CollectI exI conjI)
-    show "00 = (#0::real) (*) x" by (simp!)
+    show "0 = (#0::real) \<cdot> x" by (simp!)
   qed simp
 
   show "lin x <= V"
   proof (unfold lin_def, intro subsetI, elim CollectE exE conjE) 
-    fix xa a assume "xa = a (*) x" 
-    show "xa:V" by (simp!)
+    fix xa a assume "xa = a \<cdot> x" 
+    show "xa \<in> V" by (simp!)
   qed
 
-  show "ALL x1 : lin x. ALL x2 : lin x. x1 + x2 : lin x" 
+  show "\<forall>x1 \<in> lin x. \<forall>x2 \<in> lin x. x1 + x2 \<in> lin x" 
   proof (intro ballI)
-    fix x1 x2 assume "x1 : lin x" "x2 : lin x" 
-    thus "x1 + x2 : lin x"
+    fix x1 x2 assume "x1 \<in> lin x" "x2 \<in> lin x" 
+    thus "x1 + x2 \<in> lin x"
     proof (unfold lin_def, elim CollectE exE conjE, 
       intro CollectI exI conjI)
-      fix a1 a2 assume "x1 = a1 (*) x" "x2 = a2 (*) x"
-      show "x1 + x2 = (a1 + a2) (*) x" 
+      fix a1 a2 assume "x1 = a1 \<cdot> x" "x2 = a2 \<cdot> x"
+      show "x1 + x2 = (a1 + a2) \<cdot> x" 
         by (simp! add: vs_add_mult_distrib2)
     qed simp
   qed
 
-  show "ALL xa:lin x. ALL a. a (*) xa : lin x" 
+  show "\<forall>xa \<in> lin x. \<forall>a. a \<cdot> xa \<in> lin x" 
   proof (intro ballI allI)
-    fix x1 a assume "x1 : lin x" 
-    thus "a (*) x1 : lin x"
+    fix x1 a assume "x1 \<in> lin x" 
+    thus "a \<cdot> x1 \<in> lin x"
     proof (unfold lin_def, elim CollectE exE conjE,
       intro CollectI exI conjI)
-      fix a1 assume "x1 = a1 (*) x"
-      show "a (*) x1 = (a * a1) (*) x" by (simp!)
+      fix a1 assume "x1 = a1 \<cdot> x"
+      show "a \<cdot> x1 = (a * a1) \<cdot> x" by (simp!)
     qed simp
   qed 
 qed
@@ -199,9 +199,9 @@
 text {* Any linear closure is a vector space. *}
 
 lemma lin_vs [intro??]: 
-  "[| is_vectorspace V; x:V |] ==> is_vectorspace (lin x)"
+  "[| is_vectorspace V; x \<in> V |] ==> is_vectorspace (lin x)"
 proof (rule subspace_vs)
-  assume "is_vectorspace V" "x:V"
+  assume "is_vectorspace V" "x \<in> V"
   show "is_subspace (lin x) V" ..
 qed
 
@@ -215,22 +215,22 @@
 instance set :: (plus) plus by intro_classes
 
 defs vs_sum_def:
-  "U + V == {u + v | u v. u:U & v:V}" (***
+  "U + V == {u + v | u v. u \<in> U \<and> v \<in> V}" (***
 
 constdefs 
   vs_sum :: 
-  "['a::{minus, plus} set, 'a set] => 'a set"         (infixl "+" 65)
-  "vs_sum U V == {x. EX u:U. EX v:V. x = u + v}";
+  "['a::{plus, minus, zero} set, 'a set] => 'a set"         (infixl "+" 65)
+  "vs_sum U V == {x. \<exists>u \<in> U. \<exists>v \<in> V. x = u + v}";
 ***)
 
 lemma vs_sumD: 
-  "x: U + V = (EX u:U. EX v:V. x = u + v)"
+  "x \<in> U + V = (\<exists>u \<in> U. \<exists>v \<in> V. x = u + v)"
     by (unfold vs_sum_def) fast
 
 lemmas vs_sumE = vs_sumD [RS iffD1, elimify]
 
 lemma vs_sumI [intro??]: 
-  "[| x:U; y:V; t= x + y |] ==> t : U + V"
+  "[| x \<in> U; y \<in> V; t= x + y |] ==> t \<in> U + V"
   by (unfold vs_sum_def) fast
 
 text{* $U$ is a subspace of $U + V$. *}
@@ -240,20 +240,20 @@
   ==> is_subspace U (U + V)"
 proof 
   assume "is_vectorspace U" "is_vectorspace V"
-  show "00 : U" ..
+  show "0 \<in> U" ..
   show "U <= U + V"
   proof (intro subsetI vs_sumI)
-  fix x assume "x:U"
-    show "x = x + 00" by (simp!)
-    show "00 : V" by (simp!)
+  fix x assume "x \<in> U"
+    show "x = x + 0" by (simp!)
+    show "0 \<in> V" by (simp!)
   qed
-  show "ALL x:U. ALL y:U. x + y : U" 
+  show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U" 
   proof (intro ballI)
-    fix x y assume "x:U" "y:U" show "x + y : U" by (simp!)
+    fix x y assume "x \<in> U" "y \<in> U" show "x + y \<in> U" by (simp!)
   qed
-  show "ALL x:U. ALL a. a (*) x : U" 
+  show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U" 
   proof (intro ballI allI)
-    fix x a assume "x:U" show "a (*) x : U" by (simp!)
+    fix x a assume "x \<in> U" show "a \<cdot> x \<in> U" by (simp!)
   qed
 qed
 
@@ -264,38 +264,38 @@
   ==> is_subspace (U + V) E"
 proof 
   assume "is_subspace U E" "is_subspace V E" "is_vectorspace E"
-  show "00 : U + V"
+  show "0 \<in> U + V"
   proof (intro vs_sumI)
-    show "00 : U" ..
-    show "00 : V" ..
-    show "(00::'a) = 00 + 00" by (simp!)
+    show "0 \<in> U" ..
+    show "0 \<in> V" ..
+    show "(0::'a) = 0 + 0" by (simp!)
   qed
   
   show "U + V <= E"
   proof (intro subsetI, elim vs_sumE bexE)
-    fix x u v assume "u : U" "v : V" "x = u + v"
-    show "x:E" by (simp!)
+    fix x u v assume "u \<in> U" "v \<in> V" "x = u + v"
+    show "x \<in> E" by (simp!)
   qed
   
-  show "ALL x: U + V. ALL y: U + V. x + y : U + V"
+  show "\<forall>x \<in> U + V. \<forall>y \<in> U + V. x + y \<in> U + V"
   proof (intro ballI)
-    fix x y assume "x : U + V" "y : U + V"
-    thus "x + y : U + V"
+    fix x y assume "x \<in> U + V" "y \<in> U + V"
+    thus "x + y \<in> U + V"
     proof (elim vs_sumE bexE, intro vs_sumI)
       fix ux vx uy vy 
-      assume "ux : U" "vx : V" "x = ux + vx" 
-	and "uy : U" "vy : V" "y = uy + vy"
+      assume "ux \<in> U" "vx \<in> V" "x = ux + vx" 
+	and "uy \<in> U" "vy \<in> V" "y = uy + vy"
       show "x + y = (ux + uy) + (vx + vy)" by (simp!)
     qed (simp!)+
   qed
 
-  show "ALL x : U + V. ALL a. a (*) x : U + V"
+  show "\<forall>x \<in> U + V. \<forall>a. a \<cdot> x \<in> U + V"
   proof (intro ballI allI)
-    fix x a assume "x : U + V"
-    thus "a (*) x : U + V"
+    fix x a assume "x \<in> U + V"
+    thus "a \<cdot> x \<in> U + V"
     proof (elim vs_sumE bexE, intro vs_sumI)
-      fix a x u v assume "u : U" "v : V" "x = u + v"
-      show "a (*) x = (a (*) u) + (a (*) v)" 
+      fix a x u v assume "u \<in> U" "v \<in> V" "x = u + v"
+      show "a \<cdot> x = (a \<cdot> u) + (a \<cdot> v)" 
         by (simp! add: vs_add_mult_distrib1)
     qed (simp!)+
   qed
@@ -323,154 +323,154 @@
 
 lemma decomp: 
   "[| is_vectorspace E; is_subspace U E; is_subspace V E; 
-  U Int V = {00}; u1:U; u2:U; v1:V; v2:V; u1 + v1 = u2 + v2 |] 
-  ==> u1 = u2 & v1 = v2" 
+  U \<inter> V = {0}; u1 \<in> U; u2 \<in> U; v1 \<in> V; v2 \<in> V; u1 + v1 = u2 + v2 |] 
+  ==> u1 = u2 \<and> v1 = v2" 
 proof 
   assume "is_vectorspace E" "is_subspace U E" "is_subspace V E"  
-    "U Int V = {00}" "u1:U" "u2:U" "v1:V" "v2:V" 
+    "U \<inter> V = {0}" "u1 \<in> U" "u2 \<in> U" "v1 \<in> V" "v2 \<in> V" 
     "u1 + v1 = u2 + v2" 
   have eq: "u1 - u2 = v2 - v1" by (simp! add: vs_add_diff_swap)
-  have u: "u1 - u2 : U" by (simp!) 
-  with eq have v': "v2 - v1 : U" by simp 
-  have v: "v2 - v1 : V" by (simp!) 
-  with eq have u': "u1 - u2 : V" by simp
+  have u: "u1 - u2 \<in> U" by (simp!) 
+  with eq have v': "v2 - v1 \<in> U" by simp 
+  have v: "v2 - v1 \<in> V" by (simp!) 
+  with eq have u': "u1 - u2 \<in> V" by simp
   
   show "u1 = u2"
   proof (rule vs_add_minus_eq)
-    show "u1 - u2 = 00" by (rule Int_singletonD [OF _ u u']) 
-    show "u1 : E" ..
-    show "u2 : E" ..
+    show "u1 - u2 = 0" by (rule Int_singletonD [OF _ u u']) 
+    show "u1 \<in> E" ..
+    show "u2 \<in> E" ..
   qed
 
   show "v1 = v2"
   proof (rule vs_add_minus_eq [RS sym])
-    show "v2 - v1 = 00" by (rule Int_singletonD [OF _ v' v])
-    show "v1 : E" ..
-    show "v2 : E" ..
+    show "v2 - v1 = 0" by (rule Int_singletonD [OF _ v' v])
+    show "v1 \<in> E" ..
+    show "v2 \<in> E" ..
   qed
 qed
 
 text {* An application of the previous lemma will be used in the proof
-of the Hahn-Banach Theorem (see page \pageref{decomp-H0-use}): for any
+of the Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any
 element $y + a \mult x_0$ of the direct sum of a vectorspace $H$ and
 the linear closure of $x_0$ the components $y \in H$ and $a$ are
 uniquely determined. *}
 
-lemma decomp_H0: 
-  "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; 
-  x0 ~: H; x0 : E; x0 ~= 00; y1 + a1 (*) x0 = y2 + a2 (*) x0 |]
-  ==> y1 = y2 & a1 = a2"
+lemma decomp_H': 
+  "[| is_vectorspace E; is_subspace H E; y1 \<in> H; y2 \<in> H; 
+  x' \<notin> H; x' \<in> E; x' \<noteq> 0; y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x' |]
+  ==> y1 = y2 \<and> a1 = a2"
 proof
   assume "is_vectorspace E" and h: "is_subspace H E"
-     and "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= 00" 
-         "y1 + a1 (*) x0 = y2 + a2 (*) x0"
+     and "y1 \<in> H" "y2 \<in> H" "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0" 
+         "y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x'"
 
-  have c: "y1 = y2 & a1 (*) x0 = a2 (*) x0"
+  have c: "y1 = y2 \<and> a1 \<cdot> x' = a2 \<cdot> x'"
   proof (rule decomp) 
-    show "a1 (*) x0 : lin x0" .. 
-    show "a2 (*) x0 : lin x0" ..
-    show "H Int (lin x0) = {00}" 
+    show "a1 \<cdot> x' \<in> lin x'" .. 
+    show "a2 \<cdot> x' \<in> lin x'" ..
+    show "H \<inter> (lin x') = {0}" 
     proof
-      show "H Int lin x0 <= {00}" 
+      show "H \<inter> lin x' <= {0}" 
       proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2])
-        fix x assume "x:H" "x : lin x0" 
-        thus "x = 00"
+        fix x assume "x \<in> H" "x \<in> lin x'" 
+        thus "x = 0"
         proof (unfold lin_def, elim CollectE exE conjE)
-          fix a assume "x = a (*) x0"
+          fix a assume "x = a \<cdot> x'"
           show ?thesis
           proof cases
             assume "a = (#0::real)" show ?thesis by (simp!)
           next
-            assume "a ~= (#0::real)" 
-            from h have "rinv a (*) a (*) x0 : H" 
+            assume "a \<noteq> (#0::real)" 
+            from h have "rinv a \<cdot> a \<cdot> x' \<in> H" 
               by (rule subspace_mult_closed) (simp!)
-            also have "rinv a (*) a (*) x0 = x0" by (simp!)
-            finally have "x0 : H" .
+            also have "rinv a \<cdot> a \<cdot> x' = x'" by (simp!)
+            finally have "x' \<in> H" .
             thus ?thesis by contradiction
           qed
        qed
       qed
-      show "{00} <= H Int lin x0"
+      show "{0} <= H \<inter> lin x'"
       proof -
-	have "00: H Int lin x0"
+	have "0 \<in> H \<inter> lin x'"
 	proof (rule IntI)
-	  show "00:H" ..
-	  from lin_vs show "00 : lin x0" ..
+	  show "0 \<in> H" ..
+	  from lin_vs show "0 \<in> lin x'" ..
 	qed
 	thus ?thesis by simp
       qed
     qed
-    show "is_subspace (lin x0) E" ..
+    show "is_subspace (lin x') E" ..
   qed
   
   from c show "y1 = y2" by simp
   
   show  "a1 = a2" 
   proof (rule vs_mult_right_cancel [RS iffD1])
-    from c show "a1 (*) x0 = a2 (*) x0" by simp
+    from c show "a1 \<cdot> x' = a2 \<cdot> x'" by simp
   qed
 qed
 
-text {* Since for any element $y + a \mult x_0$ of the direct sum 
-of a vectorspace $H$ and the linear closure of $x_0$ the components
+text {* Since for any element $y + a \mult x'$ of the direct sum 
+of a vectorspace $H$ and the linear closure of $x'$ the components
 $y\in H$ and $a$ are unique, it follows from $y\in H$ that 
 $a = 0$.*} 
 
-lemma decomp_H0_H: 
-  "[| is_vectorspace E; is_subspace H E; t:H; x0 ~: H; x0:E;
-  x0 ~= 00 |] 
-  ==> (SOME (y, a). t = y + a (*) x0 & y : H) = (t, (#0::real))"
+lemma decomp_H'_H: 
+  "[| is_vectorspace E; is_subspace H E; t \<in> H; x' \<notin> H; x' \<in> E;
+  x' \<noteq> 0 |] 
+  ==> (SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, (#0::real))"
 proof (rule, unfold split_tupled_all)
-  assume "is_vectorspace E" "is_subspace H E" "t:H" "x0 ~: H" "x0:E"
-    "x0 ~= 00"
+  assume "is_vectorspace E" "is_subspace H E" "t \<in> H" "x' \<notin> H" "x' \<in> E"
+    "x' \<noteq> 0"
   have h: "is_vectorspace H" ..
-  fix y a presume t1: "t = y + a (*) x0" and "y:H"
-  have "y = t & a = (#0::real)" 
-    by (rule decomp_H0) (assumption | (simp!))+
+  fix y a presume t1: "t = y + a \<cdot> x'" and "y \<in> H"
+  have "y = t \<and> a = (#0::real)" 
+    by (rule decomp_H') (assumption | (simp!))+
   thus "(y, a) = (t, (#0::real))" by (simp!)
 qed (simp!)+
 
-text {* The components $y\in H$ and $a$ in $y \plus a \mult x_0$ 
-are unique, so the function $h_0$ defined by 
-$h_0 (y \plus a \mult x_0) = h y + a \cdot \xi$ is definite. *}
+text {* The components $y\in H$ and $a$ in $y \plus a \mult x'$ 
+are unique, so the function $h'$ defined by 
+$h' (y \plus a \mult x') = h y + a \cdot \xi$ is definite. *}
 
-lemma h0_definite:
-  "[| h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a (*) x0 & y:H)
+lemma h'_definite:
+  "[| h' == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H)
                 in (h y) + a * xi);
-  x = y + a (*) x0; is_vectorspace E; is_subspace H E;
-  y:H; x0 ~: H; x0:E; x0 ~= 00 |]
-  ==> h0 x = h y + a * xi"
+  x = y + a \<cdot> x'; is_vectorspace E; is_subspace H E;
+  y \<in> H; x' \<notin> H; x' \<in> E; x' \<noteq> 0 |]
+  ==> h' x = h y + a * xi"
 proof -  
   assume 
-    "h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a (*) x0 & y:H)
+    "h' == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H)
                in (h y) + a * xi)"
-    "x = y + a (*) x0" "is_vectorspace E" "is_subspace H E"
-    "y:H" "x0 ~: H" "x0:E" "x0 ~= 00"
-  have "x : H + (lin x0)" 
+    "x = y + a \<cdot> x'" "is_vectorspace E" "is_subspace H E"
+    "y \<in> H" "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0"
+  have "x \<in> H + (lin x')" 
     by (simp! add: vs_sum_def lin_def) force+
-  have "EX! xa. ((\\<lambda>(y, a). x = y + a (*) x0 & y:H) xa)" 
+  have "\<exists>! xa. ((\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) xa)" 
   proof
-    show "EX xa. ((\\<lambda>(y, a). x = y + a (*) x0 & y:H) xa)"
+    show "\<exists>xa. ((\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) xa)"
       by (force!)
   next
     fix xa ya
-    assume "(\\<lambda>(y,a). x = y + a (*) x0 & y : H) xa"
-           "(\\<lambda>(y,a). x = y + a (*) x0 & y : H) ya"
+    assume "(\<lambda>(y,a). x = y + a \<cdot> x' \<and> y \<in> H) xa"
+           "(\<lambda>(y,a). x = y + a \<cdot> x' \<and> y \<in> H) ya"
     show "xa = ya" 
     proof -
-      show "fst xa = fst ya & snd xa = snd ya ==> xa = ya" 
+      show "fst xa = fst ya \<and> snd xa = snd ya ==> xa = ya" 
         by (simp add: Pair_fst_snd_eq)
-      have x: "x = fst xa + snd xa (*) x0 & fst xa : H" 
+      have x: "x = fst xa + snd xa \<cdot> x' \<and> fst xa \<in> H" 
         by (force!)
-      have y: "x = fst ya + snd ya (*) x0 & fst ya : H" 
+      have y: "x = fst ya + snd ya \<cdot> x' \<and> fst ya \<in> H" 
         by (force!)
-      from x y show "fst xa = fst ya & snd xa = snd ya" 
-        by (elim conjE) (rule decomp_H0, (simp!)+)
+      from x y show "fst xa = fst ya \<and> snd xa = snd ya" 
+        by (elim conjE) (rule decomp_H', (simp!)+)
     qed
   qed
-  hence eq: "(SOME (y, a). x = y + a (*) x0 & y:H) = (y, a)" 
+  hence eq: "(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) = (y, a)" 
     by (rule select1_equality) (force!)
-  thus "h0 x = h y + a * xi" by (simp! add: Let_def)
+  thus "h' x = h y + a * xi" by (simp! add: Let_def)
 qed
 
 end
\ No newline at end of file
diff -r 78a11a353473 -r 153853af318b src/HOL/Real/HahnBanach/VectorSpace.thy
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Sun Jul 16 21:00:32 2000 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Mon Jul 17 13:58:18 2000 +0200
@@ -15,24 +15,11 @@
 element $\zero$ is defined. *}
 
 consts
-  prod  :: "[real, 'a] => 'a"                       (infixr "'(*')" 70)
-  zero  :: 'a                                       ("00")
+  prod  :: "[real, 'a::{plus, minus, zero}] => 'a"        (infixr "'(*')" 70)
 
 syntax (symbols)
-  prod  :: "[real, 'a] => 'a"                       (infixr "\<prod>" 70)
-  zero  :: 'a                                       ("\<zero>")
-
-(* text {* The unary and binary minus can be considered as 
-abbreviations: *}
-*)
+  prod  :: "[real, 'a] => 'a"                       (infixr "\<cdot>" 70)
 
-(***
-constdefs 
-  negate :: "'a => 'a"                           ("- _" [100] 100)
-  "- x == (- #1) ( * ) x"
-  diff :: "'a => 'a => 'a"                       (infixl "-" 68)
-  "x - y == x + - y";
-***)
 
 subsection {* Vector space laws *}
 
@@ -47,43 +34,43 @@
 *}
 
 constdefs
-  is_vectorspace :: "('a::{plus,minus}) set => bool"
-  "is_vectorspace V == V ~= {} 
-   & (ALL x:V. ALL y:V. ALL z:V. ALL a b.
-        x + y : V                                 
-      & a (*) x : V                                 
-      & (x + y) + z = x + (y + z)             
-      & x + y = y + x                           
-      & x - x = 00                               
-      & 00 + x = x                               
-      & a (*) (x + y) = a (*) x + a (*) y       
-      & (a + b) (*) x = a (*) x + b (*) x         
-      & (a * b) (*) x = a (*) b (*) x               
-      & #1 (*) x = x
-      & - x = (- #1) (*) x
-      & x - y = x + - y)"                             
+  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)"                             
 
 text_raw {* \medskip *}
 text {* The corresponding introduction rule is:*}
 
 lemma vsI [intro]:
-  "[| 00:V; 
-  ALL x:V. ALL y:V. x + y : V; 
-  ALL x:V. ALL a. a (*) x : V;  
-  ALL x:V. ALL y:V. ALL z:V. (x + y) + z = x + (y + z);
-  ALL x:V. ALL y:V. x + y = y + x;
-  ALL x:V. x - x = 00;
-  ALL x:V. 00 + x = x;
-  ALL x:V. ALL y:V. ALL a. a (*) (x + y) = a (*) x + a (*) y;
-  ALL x:V. ALL a b. (a + b) (*) x = a (*) x + b (*) x;
-  ALL x:V. ALL a b. (a * b) (*) x = a (*) b (*) x; 
-  ALL x:V. #1 (*) x = x; 
-  ALL x:V. - x = (- #1) (*) x; 
-  ALL x:V. ALL y: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:V" "y:V" "z:V"
-    "ALL x:V. ALL y:V. ALL z: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 (elim bspec[elimify])
 qed force+
 
@@ -91,58 +78,58 @@
 text {* The corresponding destruction rules are: *}
 
 lemma negate_eq1: 
-  "[| is_vectorspace V; x:V |] ==> - x = (- #1) (*) x"
+  "[| is_vectorspace V; x \<in> V |] ==> - x = (- #1) \<cdot> x"
   by (unfold is_vectorspace_def) simp
 
 lemma diff_eq1: 
-  "[| is_vectorspace V; x:V; y: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:V |] ==> (- #1) (*) 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:V |] ==> #-1 (*) 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:V; y: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 ~= {})" 
+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:V; y:V |] ==> x + y : 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:V |] ==> a (*) x : 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:V; y:V |] ==> x - y : 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:V |] ==> - x : V"
+  "[| is_vectorspace V; x \<in> V |] ==> - x \<in> V"
   by (simp add: negate_eq1)
 
 lemma vs_add_assoc [simp]:  
-  "[| is_vectorspace V; x:V; y:V; z: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:V; y: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:V; y:V; z: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:V" "y:V" "z: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)
@@ -153,78 +140,78 @@
 theorems vs_add_ac = vs_add_assoc vs_add_commute vs_add_left_commute
 
 lemma vs_diff_self [simp]: 
-  "[| is_vectorspace V; x:V |] ==>  x - x = 00" 
+  "[| 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 ==> 00:V"
+lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> 0 \<in> V"
 proof - 
   assume "is_vectorspace V"
-  have "V ~= {}" ..
-  hence "EX x. x:V" by force
+  have "V \<noteq> {}" ..
+  hence "\<exists>x. x \<in> V" by force
   thus ?thesis 
   proof 
-    fix x assume "x:V" 
-    have "00 = x - x" by (simp!)
-    also have "... : V" by (simp! only: vs_diff_closed)
+    fix x assume "x \<in> V" 
+    have "0 = x - x" by (simp!)
+    also have "... \<in> V" by (simp! only: vs_diff_closed)
     finally show ?thesis .
   qed
 qed
 
 lemma vs_add_zero_left [simp]: 
-  "[| is_vectorspace V; x:V |] ==>  00 + 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:V |] ==>  x + 00 = x"
+  "[| is_vectorspace V; x \<in> V |] ==>  x + 0 = x"
 proof -
-  assume "is_vectorspace V" "x:V"
-  hence "x + 00 = 00 + x" by simp
+  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:V; y:V |] 
-  ==> a (*) (x + y) = a (*) x + a (*) 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:V |] 
-  ==> (a + b) (*) x = a (*) x + b (*) 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:V |] ==> (a * b) (*) x = a (*) (b (*) 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:V |] ==> a (*) b (*) x = (a * b) (*) 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:V |] ==> #1 (*) 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:V; y:V |] 
-  ==> a (*) (x - y) = a (*) x - a (*) 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:V |] 
-  ==> (a - b) (*) x = a (*) x - (b (*) x)"
+  "[| is_vectorspace V; x \<in> V |] 
+  ==> (a - b) \<cdot> x = a \<cdot> x - (b \<cdot> x)"
 proof -
-  assume "is_vectorspace V" "x:V"
-  have " (a - b) (*) x = (a + - b) (*) 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 (*) x + (- b) (*) x" 
+  also have "... = a \<cdot> x + (- b) \<cdot> x" 
     by (rule vs_add_mult_distrib2)
-  also have "... = a (*) x + - (b (*) x)" 
+  also have "... = a \<cdot> x + - (b \<cdot> x)" 
     by (simp! add: negate_eq1)
-  also have "... = a (*) x - (b (*) x)" 
+  also have "... = a \<cdot> x - (b \<cdot> x)" 
     by (simp! add: diff_eq1)
   finally show ?thesis .
 qed
@@ -234,40 +221,40 @@
 text{* Further derived laws: *}
 
 lemma vs_mult_zero_left [simp]: 
-  "[| is_vectorspace V; x:V |] ==> #0 (*) x = 00"
+  "[| is_vectorspace V; x \<in> V |] ==> #0 \<cdot> x = 0"
 proof -
-  assume "is_vectorspace V" "x:V"
-  have  "#0 (*) x = (#1 - #1) (*) x" by simp
-  also have "... = (#1 + - #1) (*) x" by simp
-  also have "... =  #1 (*) x + (- #1) (*) 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) (*) 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 "... = 00" by (simp!)
+  also have "... = 0" by (simp!)
   finally show ?thesis .
 qed
 
 lemma vs_mult_zero_right [simp]: 
-  "[| is_vectorspace (V:: 'a::{plus, minus} set) |] 
-  ==> a (*) 00 = (00::'a)"
+  "[| is_vectorspace (V:: 'a::{plus, minus, zero} set) |] 
+  ==> a \<cdot> 0 = (0::'a)"
 proof -
   assume "is_vectorspace V"
-  have "a (*) 00 = a (*) (00 - (00::'a))" by (simp!)
-  also have "... =  a (*) 00 - a (*) 00"
+  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 "... = 00" by (simp!)
+  also have "... = 0" by (simp!)
   finally show ?thesis .
 qed
 
 lemma vs_minus_mult_cancel [simp]:  
-  "[| is_vectorspace V; x:V |] ==> (- a) (*) - x = a (*) 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:V; y:V |] ==> - x + y = y - x"
+  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> - x + y = y - x"
 proof - 
-  assume "is_vectorspace V" "x:V" "y:V"
+  assume "is_vectorspace V" "x \<in> V" "y \<in> V"
   have "- x + y = y + - x" 
     by (simp! add: vs_add_commute [RS sym, of V "- x"])
   also have "... = y - x" by (simp! add: diff_eq1)
@@ -275,63 +262,63 @@
 qed
 
 lemma vs_add_minus [simp]: 
-  "[| is_vectorspace V; x:V |] ==> x + - x = 00"
+  "[| is_vectorspace V; x \<in> V |] ==> x + - x = 0"
   by (simp! add: diff_eq2)
 
 lemma vs_add_minus_left [simp]: 
-  "[| is_vectorspace V; x:V |] ==> - x + x = 00"
+  "[| is_vectorspace V; x \<in> V |] ==> - x + x = 0"
   by (simp! add: diff_eq2)
 
 lemma vs_minus_minus [simp]: 
-  "[| is_vectorspace V; x:V |] ==> - (- x) = x"
+  "[| is_vectorspace V; x \<in> V |] ==> - (- x) = x"
   by (simp add: negate_eq1)
 
 lemma vs_minus_zero [simp]: 
-  "is_vectorspace (V::'a::{minus, plus} set) ==> - (00::'a) = 00" 
+  "is_vectorspace (V::'a::{plus, minus, zero} set) ==> - (0::'a) = 0" 
   by (simp add: negate_eq1)
 
 lemma vs_minus_zero_iff [simp]:
-  "[| is_vectorspace V; x:V |] ==> (- x = 00) = (x = 00)" 
+  "[| is_vectorspace V; x \<in> V |] ==> (- x = 0) = (x = 0)" 
   (concl is "?L = ?R")
 proof -
-  assume "is_vectorspace V" "x:V"
+  assume "is_vectorspace V" "x \<in> V"
   show "?L = ?R"
   proof
     have "x = - (- x)" by (rule vs_minus_minus [RS sym])
     also assume ?L
-    also have "- ... = 00" by (rule vs_minus_zero)
+    also have "- ... = 0" by (rule vs_minus_zero)
     finally show ?R .
   qed (simp!)
 qed
 
 lemma vs_add_minus_cancel [simp]:  
-  "[| is_vectorspace V; x:V; y: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:V; y: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:V; y: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:V |] ==> x - 00 = 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:V |] ==> 00 - 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:V; y:V; z: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:V" "y:V" "z:V"
-  have "y = 00 + y" by (simp!)
+  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)" 
     by (simp! only: vs_add_assoc vs_neg_closed)
@@ -343,68 +330,67 @@
 qed force
 
 lemma vs_add_right_cancel: 
-  "[| is_vectorspace V; x:V; y:V; z: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:V; y:V; x':V; y':V; z: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:V; y:V; z:V |] 
-  ==> x (*) y (*) z = y (*) x (*) 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:V; a (*) x = 00; x ~= 00 |] ==> a = #0"
+lemma vs_mult_zero_uniq:
+  "[| is_vectorspace V; x \<in> V; a \<cdot> x = 0; x \<noteq> 0 |] ==> a = #0"
 proof (rule classical)
-  assume "is_vectorspace V" "x:V" "a (*) x = 00" "x ~= 00"
-  assume "a ~= #0"
-  have "x = (rinv a * a) (*) x" by (simp!)
-  also have "... = rinv a (*) (a (*) x)" by (rule vs_mult_assoc)
-  also have "... = rinv a (*) 00" by (simp!)
-  also have "... = 00" by (simp!)
-  finally have "x = 00" .
+  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:V; y:V; a ~= #0 |] ==> 
-  (a (*) x = a (*) 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:V" "y:V" "a ~= #0"
-  have "x = #1 (*) x" by (simp!)
-  also have "... = (rinv a * a) (*) x" by (simp!)
-  also have "... = rinv a (*) (a (*) 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 (*) ... = 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:V; x ~= 00 |] 
-  ==> (a (*) x = b (*) 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:V" "x ~= 00"
-  have "(a - b) (*) x = a (*) x - b (*) 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 (*) x - b (*) x = 00" by (simp!)
-  finally have "(a - b) (*) x = 00" . 
+  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 (*** 
 
-backward :
 lemma vs_mult_right_cancel: 
-  "[| is_vectorspace V; x:V; x ~= 00 |] ==>  
+  "[| 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 ~= 00";
+  assume "is_vectorspace V" "x:V" "x \<noteq> 0";
   assume l: ?L; 
   show "a = b"; 
   proof (rule real_add_minus_eq);
@@ -412,8 +398,8 @@
     proof (rule vs_mult_zero_uniq);
       have "(a - b) ( * ) x = a ( * ) x - b ( * ) x";
         by (simp! add: vs_diff_mult_distrib2);
-      also; from l; have "a ( * ) x - b ( * ) x = 00"; by (simp!);
-      finally; show "(a - b) ( * ) x  = 00"; .; 
+      also; from l; have "a ( * ) x - b ( * ) x = 0"; by (simp!);
+      finally; show "(a - b) ( * ) x  = 0"; .; 
     qed;
   qed;
 next;
@@ -423,11 +409,11 @@
 **)
 
 lemma vs_eq_diff_eq: 
-  "[| is_vectorspace V; x:V; y:V; z: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:V" "y:V" "z:V"
+  assume vs: "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V"
   show "?L = ?R"   
   proof
     assume ?L
@@ -435,7 +421,7 @@
     also have "... = z + - y + y" by (simp! add: diff_eq1)
     also have "... = z + (- y + y)" 
       by (rule vs_add_assoc) (simp!)+
-    also from vs have "... = z + 00" 
+    also from vs have "... = z + 0" 
       by (simp only: vs_add_minus_left)
     also from vs have "... = z" by (simp only: vs_add_zero_right)
     finally show ?R .
@@ -452,32 +438,32 @@
 qed
 
 lemma vs_add_minus_eq_minus: 
-  "[| is_vectorspace V; x:V; y:V; x + y = 00 |] ==> x = - y" 
+  "[| is_vectorspace V; x \<in> V; y \<in> V; x + y = 0 |] ==> x = - y" 
 proof -
-  assume "is_vectorspace V" "x:V" "y: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 = 00"
-  also have "- y + 00 = - y" by (simp!)
+  also assume "x + y = 0"
+  also have "- y + 0 = - y" by (simp!)
   finally show "x = - y" .
 qed
 
 lemma vs_add_minus_eq: 
-  "[| is_vectorspace V; x:V; y:V; x - y = 00 |] ==> x = y" 
+  "[| is_vectorspace V; x \<in> V; y \<in> V; x - y = 0 |] ==> x = y" 
 proof -
-  assume "is_vectorspace V" "x:V" "y:V" "x - y = 00"
-  assume "x - y = 00"
-  hence e: "x + - y = 00" by (simp! add: diff_eq1)
+  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)" 
     by (rule vs_add_minus_eq_minus) (simp!)+
   thus "x = y" by (simp!)
 qed
 
 lemma vs_add_diff_swap:
-  "[| is_vectorspace V; a:V; b:V; c:V; d: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:V" "b:V" "c:V" "d: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)
@@ -487,16 +473,16 @@
     by (simp add: vs_add_ac diff_eq1)
   also from eq have "...  = d + - b" 
     by (simp! add: vs_add_right_cancel)
-  also have "... = d - b" by (simp! add : diff_eq2)
+  also have "... = d - b" by (simp! add: diff_eq2)
   finally show "a - c = d - b" .
 qed
 
 lemma vs_add_cancel_21: 
-  "[| is_vectorspace V; x:V; y:V; z:V; u: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:V" "y:V""z:V" "u: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!)
@@ -510,20 +496,20 @@
 qed
 
 lemma vs_add_cancel_end: 
-  "[| is_vectorspace V;  x:V; y:V; z: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:V" "y:V" "z:V"
+  assume "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V"
   show "?L = ?R"
   proof
     assume l: ?L
-    have "x + z = 00" 
+    have "x + z = 0" 
     proof (rule vs_add_left_cancel [RS iffD1])
       have "y + (x + z) = x + (y + z)" by (simp!)
       also note l
-      also have "y = y + 00" by (simp!)
-      finally show "y + (x + z) = y + 00" .
+      also have "y = y + 0" by (simp!)
+      finally show "y + (x + z) = y + 0" .
     qed (simp!)+
     thus "x = - z" by (simp! add: vs_add_minus_eq_minus)
   next