# HG changeset patch
# User bauerg
# Date 962879256 -7200
# Node ID 879e0f0cd04703ba80db4eb580bc574b607bf4ba
# Parent  678e718a5a8649f68f130279e88c9d7820deaec0
removed sorry;

diff -r 678e718a5a86 -r 879e0f0cd047 src/HOL/Real/HahnBanach/HahnBanach.thy
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Jul 06 12:15:05 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Jul 06 12:27:36 2000 +0200
@@ -19,19 +19,19 @@
     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$. *}
     proof (unfold M_def, rule norm_pres_extensionI)
-      show "EX (H::'a set) h::'a => real. graph H h = Union c
+      show "\\<exists> H h. graph H h = \\<Union> c
               & is_linearform H h 
               & is_subspace H E 
               & is_subspace F H 
-              & graph F f <= graph H h
-              & (ALL x::'a:H. h x <= p x)"
+              & graph F f \\<subseteq> graph H h
+              & (\\<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) : Union c" "(x, z) : 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" 
@@ -42,10 +42,10 @@
         show "is_subspace F ?H" 
           by (rule sup_supF [OF _ _ _ a]) (simp!)+
   (* FIXME        by (rule sup_supF, rule a) (simp!)+ *)
-        show "graph F f <= graph ?H ?h" 
+        show "graph F f \\<subseteq> graph ?H ?h" 
           by (rule sup_ext [OF _ _ _ a]) (simp!)+
   (*  FIXME      by (rule sup_ext, rule a) (simp!)+*)
-        show "ALL x::'a:?H. ?h x <= p x" 
+        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!)+ *)
       qed
@@ -56,12 +56,12 @@
   txt {* 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 : norm_pres_extensions E p F f"
+    have "graph F f \\<in> norm_pres_extensions E p F f"
     proof (rule norm_pres_extensionI2)
       have "is_vectorspace F" ..
       thus "is_subspace F F" ..
     qed (blast!)+ 
-    thus "graph F f : M" by (simp!)
+    thus "graph F f \\<in> M" by (simp!)
   qed
   thus ?thesis
   proof
@@ -75,10 +75,10 @@
         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 *}
       proof -
-        have "EX H h. graph H h = g & is_linearform H h 
+        have "\\<exists> 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)" by (simp! add: norm_pres_extension_D)
+          & graph F f \\<subseteq> graph H h
+          & (\\<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" ..
@@ -92,26 +92,52 @@
           obtain x' where "x' \\<in> E" "x' \\<notin> H" 
           txt {* Pick $x' \in E \setminus H$. \skp *}
           proof -
-            have "EX x':E. x'~:H"
+            have "\\<exists>x' \\<in> E. x' \\<notin> H"
             proof (rule set_less_imp_diff_not_empty)
-              have "H <= E" ..
-              thus "H < E" ..
+              have "H \\<subseteq> E" ..
+              thus "H \\<subset> E" ..
             qed
             thus ?thesis by blast
           qed
-          have x': "x' ~= \<zero>"
+          have x': "x' \\<noteq> \<zero>"
           proof (rule classical)
             presume "x' = \<zero>"
-            with h have "x':H" by simp
+            with h have "x' \\<in> H" by simp
             thus ?thesis by contradiction
           qed blast
           def H' == "H + lin x'"
           -- {* Define $H'$ as the direct sum of $H$ and the linear closure of $x'$. \skp *}
           show ?thesis
             obtain xi where "\\<forall>y \\<in> H. - p (y + x') - h y \\<le> xi 
-                              \\<and> xi \\<le> p (y + x') - h y" sorry
-            -- {* Pick a real number $\xi$ that fulfills certain inequations; this will *}
-            -- {* be used to establish that $h'$ is a norm-preserving extension of $h$. \skp *}
+                              \\<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 *}
+
+            proof -
+	      from h have "EX xi. ALL y:H. - p (y + x') - h y <= xi 
+                              & xi <= p (y + x') - h y" 
+              proof (rule ex_xi)
+                fix u v assume "u:H" "v:H"
+                from h have "h v - h u = h (v - u)"
+                  by (simp! add: linearform_diff)
+                also have "... <= p (v - u)"
+                  by (simp!)
+                also have "v - u = x' + - x' + v + - u"
+                  by (simp! add: diff_eq1)
+                also have "... = v + x' + - (u + x')"
+                  by (simp!)
+                also have "... = (v + x') - (u + x')"
+                  by (simp! add: diff_eq1)
+                also have "p ... <= p (v + x') + p (u + x')"
+                  by (rule seminorm_diff_subadditive) (simp!)+
+                finally have "h v - h u <= p (v + x') + p (u + x')" .
+
+                thus "- p (u + x') - h u <= p (v + x') - h v" 
+                  by (rule real_diff_ineq_swap)
+              qed
+              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
                            in (h y) + a * xi"
             -- {* Define the extension $h'$ of $h$ to $H'$ using $\xi$. \skp *}
@@ -120,17 +146,17 @@
               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 <= graph H' h'"
+		show "g \\<subseteq> graph H' h'"
 		proof -
-		  have  "graph H h <= graph H' h'"
+		  have  "graph H h \\<subseteq> graph H' h'"
                   proof (rule graph_extI)
-		    fix t assume "t:H" 
-		    have "(SOME (y, a). t = y + a \<prod> x' & y : H)
+		    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'])
 		    thus "h t = h' t" by (simp! add: Let_def)
 		  next
-		    show "H <= H'"
+		    show "H \\<subseteq> H'"
 		    proof (rule subspace_subset)
 		      show "is_subspace H H'"
 		      proof (unfold H'_def, rule subspace_vs_sum1)
@@ -141,20 +167,20 @@
 		  qed 
 		  thus ?thesis by (simp!)
 		qed
-                show "g ~= graph H' h'"
+                show "g \\<noteq> graph H' h'"
 		proof -
-		  have "graph H h ~= graph H' h'"
+		  have "graph H h \\<noteq> graph H' h'"
 		  proof
 		    assume e: "graph H h = graph H' h'"
-		    have "x' : H'" 
+		    have "x' \\<in> H'" 
 		    proof (unfold H'_def, rule vs_sumI)
 		      show "x' = \<zero> + x'" by (simp!)
-		      from h show "\<zero> : H" ..
-		      show "x' : lin x'" by (rule x_lin_x)
+		      from h show "\<zero> \\<in> H" ..
+		      show "x' \\<in> lin x'" by (rule x_lin_x)
 		    qed
-		    hence "(x', h' x') : graph H' h'" ..
-		    with e have "(x', h' x') : graph H h" by simp
-		    hence "x' : 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!)
@@ -163,7 +189,7 @@
 	      show "graph H' h' \\<in> M" 
               txt {* and $h'$ is norm-preserving. \skp *} 
               proof -
-		have "graph H' h' : 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!)+
@@ -175,29 +201,29 @@
 		  finally (subspace_trans [OF _ h]) 
 		  show f_h': "is_subspace F H'" .
 		
-		  show "graph F f <= graph H' h'"
+		  show "graph F f \\<subseteq> graph H' h'"
 		  proof (rule graph_extI)
-		    fix x assume "x: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 : H)"
+		      "(x, #0) = (SOME (y, a). x = y + a (*) x' & y \\<in> H)"
 		      by (rule decomp_H0_H [RS sym, OF _ _ _ _ _ x']) (simp!)+
 		    also have 
-		      "(let (y,a) = (SOME (y,a). x = y + a (*) x' & y : H)
+		      "(let (y,a) = (SOME (y,a). x = y + a (*) x' & y \\<in> H)
                         in h y + a * xi) 
                       = h' x" by (simp!)
 		    finally show "f x = h' x" .
 		  next
-		    from f_h' show "F <= H'" ..
+		    from f_h' show "F \\<subseteq> H'" ..
 		  qed
 		
-		  show "ALL x:H'. h' x <= p x"
+		  show "\\<forall>x \\<in> H'. h' x \\<le> p x"
 		    by (rule h0_norm_pres [OF _ _ _ _ x'])
 		qed
-		thus "graph H' h' : M" by (simp!)
+		thus "graph H' h' \\<in> M" by (simp!)
 	      qed
             qed
           qed
@@ -211,11 +237,11 @@
       proof (intro exI conjI)
         assume eq: "H = E"
 	from eq show "is_linearform E h" by (simp!)
-	show "ALL x:F. h x = f x" 
+	show "\\<forall>x \\<in> F. h x = f x" 
 	proof (intro ballI, rule sym)
-	  fix x assume "x:F" show "f x = h x " ..
+	  fix x assume "x \\<in> F" show "f x = h x " ..
 	qed
-	from eq show "ALL x:E. h x <= p x" by (force!)
+	from eq show "\\<forall>x \\<in> E. h x \\<le> p x" by (force!)
       qed
     qed
   qed
diff -r 678e718a5a86 -r 879e0f0cd047 src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Thu Jul 06 12:15:05 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Thu Jul 06 12:27:36 2000 +0200
@@ -3,9 +3,9 @@
     Author:     Gertrud Bauer, TU Munich
 *)
 
-header {* The supremum w.r.t.~the function order *};
+header {* The supremum w.r.t.~the function order *}
 
-theory HahnBanachSupLemmas = FunctionNorm + ZornLemma:;
+theory HahnBanachSupLemmas = FunctionNorm + ZornLemma:
 
 
 
@@ -18,622 +18,472 @@
 $\Union c = \idt{graph}\ap H\ap h$. 
 We will show some properties about the limit function $h$, 
 i.e.\ the supremum of the chain $c$.
-*}; 
-
-(***
-lemma some_H'h't:
-  "[| M = norm_pres_extensions E p F f; c: chain M; 
-  graph H h = Union c; x:H |]
-   ==> EX H' h' t. t : graph H h & t = (x, h x) & graph H' h':c 
-       & t:graph H' h' & 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)";
-proof -;
-  assume m: "M = norm_pres_extensions E p F f" and cM: "c: chain M"
-     and u: "graph H h = Union c" "x:H";
-
-  let ?P = "\\<lambda>H h. 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)";
+*} 
 
-  have "EX t : graph H h. t = (x, h x)"; 
-    by (rule graphI2);
-  thus ?thesis;
-  proof (elim bexE); 
-    fix t; assume t: "t : graph H h" "t = (x, h x)";
-    with u; have ex1: "EX g:c. t:g";
-      by (simp only: Union_iff);
-    thus ?thesis;
-    proof (elim bexE);
-      fix g; assume g: "g:c" "t:g";
-      from cM; have "c <= M"; by (rule chainD2);
-      hence "g : M"; ..;
-      hence "g : norm_pres_extensions E p F f"; by (simp only: m);
-      hence "EX H' h'. graph H' h' = g & ?P H' h'"; 
-        by (rule norm_pres_extension_D);
-      thus ?thesis; 
-       by (elim exE conjE, intro exI conjI) (simp | simp!)+;
-    qed;
-  qed;
-qed;
-***)
 
 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
-one of the elements of the chain. *};
+one of the elements of the chain. *}
 
 lemma some_H'h't:
-  "[| M = norm_pres_extensions E p F f; c: chain M; 
-  graph H h = Union c; x:H |]
-   ==> EX H' h'. graph H' h' : c & (x, h x) : graph 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'. 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 <= graph H' h' 
-       & (ALL x:H'. h' x <= p x)";
-proof -;
-  assume m: "M = norm_pres_extensions E p F f" and "c: chain M"
-     and u: "graph H h = Union c" "x:H";
+       & is_subspace F H' & graph F f \\<subseteq> graph H' h' 
+       & (\\<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"
 
-  have h: "(x, h x) : graph H h"; ..;
-  with u; have "(x, h x) : Union c"; by simp;
-  hence ex1: "EX g:c. (x, h x) : g"; 
-    by (simp only: Union_iff);
-  thus ?thesis;
-  proof (elim bexE);
-    fix g; assume g: "g:c" "(x, h x) : g";
-    have "c <= M"; by (rule chainD2);
-    hence "g : M"; ..;
-    hence "g : norm_pres_extensions E p F f"; by (simp only: m);
-    hence "EX H' h'. graph H' h' = g 
+  have h: "(x, h x) \<in> graph H h" ..
+  with u have "(x, h x) \<in> Union c" by simp
+  hence ex1: "\<exists> g \\<in> c. (x, h x) \<in> g" 
+    by (simp only: Union_iff)
+  thus ?thesis
+  proof (elim bexE)
+    fix g assume g: "g \\<in> c" "(x, h x) \\<in> g"
+    have "c \\<subseteq> M" by (rule chainD2)
+    hence "g \\<in> M" ..
+    hence "g \<in> norm_pres_extensions E p F f" by (simp only: m)
+    hence "\<exists> H' h'. graph H' h' = g 
                   & 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)";
-      by (rule norm_pres_extension_D);
-    thus ?thesis;
-    proof (elim exE conjE); 
-      fix H' h'; 
+                  & graph F f \\<subseteq> graph H' h'
+                  & (\<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 <= graph H' h'" "ALL x:H'. h' x <= p x";
-      show ?thesis; 
-      proof (intro exI conjI);
-        show "graph H' h' : c"; by (simp!);
-        show "(x, h x) : graph H' h'"; by (simp!);
-      qed;
-    qed;
-  qed;
-qed;
+        "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!)
+        show "(x, h x) \<in> graph H' h'" by (simp!)
+      qed
+    qed
+  qed
+qed
 
 
 text{*  \medskip 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 the domain $H$ of the supremum function is member of
 the domain $H'$ of some function $h'$, such that $h$ extends $h'$.
-*};
+*}
 
 lemma some_H'h': 
-  "[| M = norm_pres_extensions E p F f; c: chain M; 
-  graph H h = Union c; x:H |] 
-  ==> EX H' h'. x:H' & graph H' h' <= graph 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 <= graph H' h' & (ALL x:H'. h' x <= p x)"; 
-proof -;
-  assume "M = norm_pres_extensions E p F f" and cM: "c: chain M"
-     and u: "graph H h = Union c" "x:H";  
-
-  have "EX H' h'. graph H' h' : c & (x, h x) : graph H' h' 
-       & 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)";
-    by (rule some_H'h't);
-  thus ?thesis; 
-  proof (elim exE conjE);
-    fix H' h'; assume "(x, h x) : graph H' h'" "graph H' h' : c"
-      "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";
-    show ?thesis;
-    proof (intro exI conjI);
-      show "x:H'"; by (rule graphD1);
-      from cM u; show "graph H' h' <= graph H h"; 
-        by (simp! only: chain_ball_Union_upper);
-    qed;
-  qed;
-qed;
+      & graph F f \\<subseteq> graph H' h' & (\<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"  
 
-(***
-lemma some_H'h': 
-  "[| M = norm_pres_extensions E p F f; c: chain M; 
-  graph H h = Union c; x:H |] 
-  ==> EX H' h'. x:H' & graph H' h' <= graph H h 
-      & 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)"; 
-proof -;
-  assume m: "M = norm_pres_extensions E p F f" and cM: "c: chain M"
-     and u: "graph H h = Union c" "x:H";  
-  have "(x, h x): graph H h"; by (rule graphI); 
-  hence "(x, h x) : Union c"; by (simp!);
-  hence "EX g:c. (x, h x):g"; by (simp only: Union_iff);
-  thus ?thesis; 
-  proof (elim bexE);
-    fix g; assume g: "g:c" "(x, h x):g";
-    from cM; have "c <= M"; by (rule chainD2);
-    hence "g : M"; ..;
-    hence "g : norm_pres_extensions E p F f"; by (simp only: m);
-    hence "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)"; 
-      by (rule norm_pres_extension_D);
-    thus ?thesis; 
-    proof (elim exE conjE, intro exI conjI);
-      fix H' h'; assume g': "graph H' h' = g";
-      with g; have "(x, h x): graph H' h'"; by simp;
-      thus "x:H'"; by (rule graphD1);
-      from g g'; have "graph H' h' : c"; by simp;
-      with cM u; show "graph H' h' <= graph H h"; 
-        by (simp only: chain_ball_Union_upper);
-    qed simp+;
-  qed;
-qed;
-***)
+  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)"
+    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"
+    show ?thesis
+    proof (intro exI conjI)
+      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
+qed
 
 
 text{* \medskip Any two elements $x$ and $y$ in the domain $H$ of the 
 supremum function $h$ are both in the domain $H'$ of some function 
-$h'$, such that $h$ extends $h'$. *};
+$h'$, such that $h$ extends $h'$. *}
 
 lemma some_H'h'2: 
-  "[| M = norm_pres_extensions E p F f; c: chain M; 
-  graph H h = Union c;  x:H; y:H |] 
-  ==> EX H' h'. x:H' & y:H' & graph H' h' <= graph H h 
+  "[| 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 <= graph H' h' & (ALL x:H'. h' x <= p x)"; 
-proof -;
-  assume "M = norm_pres_extensions E p F f" "c: chain M" 
-         "graph H h = Union c" "x:H" "y:H";
+      & graph F f \\<subseteq> graph H' h' & (\<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"
 
   txt {* $x$ is in the domain $H'$ of some function $h'$, 
-  such that $h$ extends $h'$. *}; 
+  such that $h$ extends $h'$. *} 
 
-  have e1: "EX H' h'. graph H' h' : c & (x, h x) : graph H' 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 <= graph H' h' 
-       & (ALL x:H'. h' x <= p x)";
-    by (rule some_H'h't);
+       & is_subspace F H' & graph F f \\<subseteq> graph H' h' 
+       & (\<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''$. *}; 
+  such that $h$ extends $h''$. *} 
 
-  have e2: "EX H'' h''. graph H'' h'' : c & (y, h y) : graph H'' 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 <= graph H'' h'' 
-       & (ALL x:H''. h'' x <= p x)";
-    by (rule some_H'h't);
+       & is_subspace F H'' & graph F f \\<subseteq> graph H'' h'' 
+       & (\<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): graph H' h'" "graph H' h' : c"
+  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"
       "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 F f \\<subseteq> graph H' h'" "\<forall> x\<in>H'. h' x \\<le> p x"
 
-    fix H'' h''; assume "(x, h x): graph H'' h''" "graph H'' h'' : 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 <= graph H'' h''" "ALL x:H''. h'' x <= 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'' <= graph H' h' | graph H' h' <= graph H'' h''"
-      (is "?case1 | ?case2");
-      by (rule chainD);
-    thus ?thesis;
-    proof; 
-      assume ?case1;
-      show ?thesis;
-      proof (intro exI conjI);
-        have "(x, h x) : graph H'' h''"; .;
-        also; have "... <= graph H' h'"; .;
-        finally; have xh: "(x, h x): graph H' h'"; .;
-        thus x: "x:H'"; ..;
-        show y: "y:H'"; ..;
-        show "graph H' h' <= graph H h";
-          by (simp! only: chain_ball_Union_upper);
-      qed;
-    next;
-      assume ?case2;
-      show ?thesis;
-      proof (intro exI conjI);
-        show x: "x:H''"; ..;
-        have "(y, h y) : graph H' h'"; by (simp!);
-        also; have "... <= graph H'' h''"; .;
-        finally; have yh: "(y, h y): graph H'' h''"; .;
-        thus y: "y:H''"; ..;
-        show "graph H'' h'' <= graph H h";
-          by (simp! only: chain_ball_Union_upper);
-      qed;
-    qed;
-  qed;
-qed;
+   $x$ and $y$ are contained in the greater one. \label{cases1}*}
 
-(***
-lemma some_H'h'2: 
-  "[| M = norm_pres_extensions E p F f; c: chain M; 
-  graph H h = Union c;  x:H; y:H |] 
-  ==> EX H' h'. x:H' & y:H' & graph H' h' <= graph H h 
-      & 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)"; 
-proof -;
-  assume "M = norm_pres_extensions E p F f" "c: chain M" 
-         "graph H h = Union c";
- 
-  let ?P = "\\<lambda>H h. 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)";
-  assume "x:H";
-  have e1: "EX H' h' t. t : graph H h & t = (x, h x) 
-            & graph H' h' : c & t : graph H' h' & ?P H' h'";
-    by (rule some_H'h't); 
-  assume "y:H";
-  have e2: "EX H' h' t. t : graph H h & t = (y, h y) 
-            & graph H' h' : c & t:graph H' h' & ?P H' h'";
-    by (rule some_H'h't); 
+    have "graph H'' h'' \\<subseteq> graph H' h' | graph H' h' \\<subseteq> graph H'' h''"
+      (is "?case1 | ?case2")
+      by (rule chainD)
+    thus ?thesis
+    proof 
+      assume ?case1
+      show ?thesis
+      proof (intro exI conjI)
+        have "(x, h x) \<in> graph H'' h''" .
+        also have "... \\<subseteq> graph H' h'" .
+        finally have xh:"(x, h x) \<in> graph H' h'" .
+        thus x: "x\<in>H'" ..
+        show y: "y\<in>H'" ..
+        show "graph H' h' \\<subseteq> graph H h"
+          by (simp! only: chain_ball_Union_upper)
+      qed
+    next
+      assume ?case2
+      show ?thesis
+      proof (intro exI conjI)
+        show x: "x\<in>H''" ..
+        have "(y, h y) \<in> graph H' h'" by (simp!)
+        also have "... \\<subseteq> graph H'' h''" .
+        finally have yh: "(y, h y)\<in> graph H'' h''" .
+        thus y: "y\<in>H''" ..
+        show "graph H'' h'' \\<subseteq> graph H h"
+          by (simp! only: chain_ball_Union_upper)
+      qed
+    qed
+  qed
+qed
 
-  from e1 e2; show ?thesis; 
-  proof (elim exE conjE);
-    fix H' h' t' H'' h'' t''; 
-    assume 
-      "t' : graph H h"             "t'' : graph H h" 
-      "t' = (y, h y)"              "t'' = (x, h x)"
-      "graph H' h' : c"            "graph H'' h'' : c"
-      "t' : graph H' h'"           "t'' : graph H'' h''" 
-      "is_linearform H' h'"        "is_linearform H'' h''"
-      "is_subspace H' E"           "is_subspace H'' E"
-      "is_subspace F H'"           "is_subspace F H''"
-      "graph F f <= graph H' h'"   "graph F f <= graph H'' h''"
-      "ALL x:H'. h' x <= p x"      "ALL x:H''. h'' x <= p x";
 
-    have "graph H'' h'' <= graph H' h' 
-         | graph H' h' <= graph H'' h''";
-      by (rule chainD);
-    thus "?thesis";
-    proof; 
-      assume "graph H'' h'' <= graph H' h'";
-      show ?thesis;
-      proof (intro exI conjI);
-        note [trans] = subsetD;
-        have "(x, h x) : graph H'' h''"; by (simp!);
-	also; have "... <= graph H' h'"; .;
-        finally; have xh: "(x, h x): graph H' h'"; .;
-	thus x: "x:H'"; by (rule graphD1);
-	show y: "y:H'"; by (simp!, rule graphD1);
-	show "graph H' h' <= graph H h";
-	  by (simp! only: chain_ball_Union_upper);
-      qed;
-    next;
-      assume "graph H' h' <= graph H'' h''";
-      show ?thesis;
-      proof (intro exI conjI);
-	show x: "x:H''"; by (simp!, rule graphD1);
-        have "(y, h y) : graph H' h'"; by (simp!);
-        also; have "... <= graph H'' h''"; .;
-	finally; have yh: "(y, h y): graph H'' h''"; .;
-        thus y: "y:H''"; by (rule graphD1);
-        show "graph H'' h'' <= graph H h";
-          by (simp! only: chain_ball_Union_upper);
-      qed;
-    qed;
-  qed;
-qed;
-
-***)
 
 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.~it is the graph of a function. *}
 
 lemma sup_definite: 
-  "[| M == norm_pres_extensions E p F f; c : chain M; 
-  (x, y) : Union c; (x, z) : Union c |] ==> z = y";
-proof -; 
-  assume "c:chain M" "M == norm_pres_extensions E p F f"
-    "(x, y) : Union c" "(x, z) : Union c";
-  thus ?thesis;
-  proof (elim UnionE chainE2);
+  "[| M == norm_pres_extensions E p F f; c \<in> chain M; 
+  (x, y) \<in> Union c; (x, z) \<in> Union c |] ==> z = y"
+proof - 
+  assume "c\<in>chain M" "M == norm_pres_extensions E p F f"
+    "(x, y) \<in> Union c" "(x, z) \<in> Union c"
+  thus ?thesis
+  proof (elim UnionE chainE2)
 
     txt{* Since both $(x, y) \in \Union c$ and $(x, z) \in \Union c$
     they are members of some graphs $G_1$ and $G_2$, resp., such that
-    both $G_1$ and $G_2$ are members of $c$.*};
+    both $G_1$ and $G_2$ are members of $c$.*}
 
-    fix G1 G2; assume
-      "(x, y) : G1" "G1 : c" "(x, z) : G2" "G2 : c" "c <= M";
+    fix G1 G2 assume
+      "(x, y) \<in> G1" "G1 \<in> c" "(x, z) \<in> G2" "G2 \<in> c" "c \\<subseteq> M"
 
-    have "G1 : M"; ..;
-    hence e1: "EX H1 h1. graph H1 h1 = G1";  
-      by (force! dest: norm_pres_extension_D);
-    have "G2 : M"; ..;
-    hence e2: "EX H2 h2. graph H2 h2 = G2";  
-      by (force! dest: norm_pres_extension_D);
-    from e1 e2; show ?thesis; 
-    proof (elim exE);
-      fix H1 h1 H2 h2; 
-      assume "graph H1 h1 = G1" "graph H2 h2 = G2";
+    have "G1 \<in> M" ..
+    hence e1: "\<exists> H1 h1. graph H1 h1 = G1"  
+      by (force! dest: norm_pres_extension_D)
+    have "G2 \<in> M" ..
+    hence e2: "\<exists> H2 h2. graph H2 h2 = G2"  
+      by (force! dest: norm_pres_extension_D)
+    from e1 e2 show ?thesis 
+    proof (elim exE)
+      fix H1 h1 H2 h2 
+      assume "graph H1 h1 = G1" "graph H2 h2 = G2"
 
       txt{* $G_1$ is contained in $G_2$ or vice versa, 
-      since both $G_1$ and $G_2$ are members of $c$. \label{cases2}*};
+      since both $G_1$ and $G_2$ are members of $c$. \label{cases2}*}
 
-      have "G1 <= G2 | G2 <= G1" (is "?case1 | ?case2"); ..;
-      thus ?thesis;
-      proof;
-        assume ?case1;
-        have "(x, y) : graph H2 h2"; by (force!);
-        hence "y = h2 x"; ..;
-        also; have "(x, z) : graph H2 h2"; by (simp!);
-        hence "z = h2 x"; ..;
-        finally; show ?thesis; .;
-      next;
-        assume ?case2;
-        have "(x, y) : graph H1 h1"; by (simp!);
-        hence "y = h1 x"; ..;
-        also; have "(x, z) : graph H1 h1"; by (force!);
-        hence "z = h1 x"; ..;
-        finally; show ?thesis; .;
-      qed;
-    qed;
-  qed;
-qed;
+      have "G1 \\<subseteq> G2 | G2 \\<subseteq> G1" (is "?case1 | ?case2") ..
+      thus ?thesis
+      proof
+        assume ?case1
+        have "(x, y) \<in> graph H2 h2" by (force!)
+        hence "y = h2 x" ..
+        also have "(x, z) \<in> graph H2 h2" by (simp!)
+        hence "z = h2 x" ..
+        finally show ?thesis .
+      next
+        assume ?case2
+        have "(x, y) \<in> graph H1 h1" by (simp!)
+        hence "y = h1 x" ..
+        also have "(x, z) \<in> graph H1 h1" by (force!)
+        hence "z = h1 x" ..
+        finally show ?thesis .
+      qed
+    qed
+  qed
+qed
 
 text{* \medskip The limit function $h$ is linear. Every element $x$ in the
 domain of $h$ is in the domain of a function $h'$ in the chain of norm
 preserving extensions.  Furthermore, $h$ is an extension of $h'$ so
 the function values of $x$ are identical for $h'$ and $h$.  Finally, the
-function $h'$ is linear by construction of $M$.  *};
+function $h'$ is linear by construction of $M$.  *}
 
 lemma sup_lf: 
-  "[| M = norm_pres_extensions E p F f; c: chain M; 
-  graph H h = Union c |] ==> is_linearform H h";
-proof -; 
-  assume "M = norm_pres_extensions E p F f" "c: chain M"
-         "graph H h = Union c";
+  "[| 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"
  
-  show "is_linearform H h";
-  proof;
-    fix x y; assume "x : H" "y : H"; 
-    have "EX H' h'. x:H' & y:H' & graph H' h' <= graph H h 
+  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 <= graph H' h'
-            & (ALL x:H'. h' x <= p x)";
-      by (rule some_H'h'2);
+            & is_subspace F H' & graph F f \\<subseteq> graph H' h'
+            & (\<forall> x\<in>H'. h' x \\<le> p x)"
+      by (rule some_H'h'2)
 
-    txt {* We have to show that $h$ is additive. *};
+    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:H'" "y:H'" 
-        and b: "graph H' h' <= graph H h" 
-        and "is_linearform H' h'" "is_subspace H' E";
-      have "h' (x + y) = h' x + h' y"; 
-        by (rule linearform_add);
-      also; have "h' x = h x"; ..;
-      also; have "h' y = h y"; ..;
-      also; have "x + y : H'"; ..;
-      with b; have "h' (x + y) = h (x + y)"; ..;
-      finally; show ?thesis; .;
-    qed;
-  next;  
-    fix a x; assume "x : H";
-    have "EX H' h'. x:H' & graph H' h' <= graph H h 
+    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" 
+        and "is_linearform H' h'" "is_subspace H' E"
+      have "h' (x + y) = h' x + h' y" 
+        by (rule linearform_add)
+      also have "h' x = h x" ..
+      also have "h' y = h y" ..
+      also have "x + y \<in> H'" ..
+      with b have "h' (x + y) = h (x + y)" ..
+      finally show ?thesis .
+    qed
+  next  
+    fix a x assume "x \<in> H"
+    have "\<exists> H' h'. x\<in>H' & graph H' h' \\<subseteq> graph H h 
             & 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)";
-      by (rule some_H'h');
+            & is_subspace F H' & graph F f \\<subseteq> graph H' h' 
+            & (\<forall> x\<in>H'. h' x \\<le> p x)"
+      by (rule some_H'h')
 
-    txt{* We have to show that $h$ is multiplicative. *};
+    txt{* We have to show that $h$ is multiplicative. *}
 
-    thus "h (a \<prod> x) = a * h x";
-    proof (elim exE conjE);
-      fix H' h'; assume "x:H'"
-        and b: "graph H' h' <= graph H h" 
-        and "is_linearform H' h'" "is_subspace H' E";
-      have "h' (a \<prod> x) = a * h' x"; 
-        by (rule linearform_mult);
-      also; have "h' x = h x"; ..;
-      also; have "a \<prod> x : H'"; ..;
-      with b; have "h' (a \<prod> x) = h (a \<prod> x)"; ..;
-      finally; show ?thesis; .;
-    qed;
-  qed;
-qed;
+    thus "h (a \<prod> x) = a * h x"
+    proof (elim exE conjE)
+      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" 
+        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)" ..
+      finally show ?thesis .
+    qed
+  qed
+qed
 
 text{* \medskip The limit of a non-empty chain of norm
 preserving extensions of $f$ is an extension of $f$,
 since every element of the chain is an extension
 of $f$ and the supremum is an extension
-for every element of the chain.*};
+for every element of the chain.*}
 
 lemma sup_ext:
-  "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c; 
-  graph H h = Union c |] ==> graph F f <= graph H h";
-proof -;
-  assume "M = norm_pres_extensions E p F f" "c: chain M" 
-         "graph H h = Union c";
-  assume "EX x. x:c";
-  thus ?thesis; 
-  proof;
-    fix x; assume "x:c"; 
-    have "c <= M"; by (rule chainD2);
-    hence "x:M"; ..;
-    hence "x : norm_pres_extensions E p F f"; by (simp!);
+  "[| 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"
+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"
+  thus ?thesis 
+  proof
+    fix x assume "x\<in>c" 
+    have "c \\<subseteq> M" by (rule chainD2)
+    hence "x\<in>M" ..
+    hence "x \<in> norm_pres_extensions E p F f" by (simp!)
 
-    hence "EX G g. graph G g = x
+    hence "\<exists> G g. graph G g = x
              & is_linearform G g 
              & is_subspace G E
              & is_subspace F G
-             & graph F f <= graph G g 
-             & (ALL x:G. g x <= p x)";
-      by (simp! add: norm_pres_extension_D);
+             & graph F f \\<subseteq> graph G g 
+             & (\<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 <= graph G g";
-      also; assume "graph G g = x";
-      also; have "... : c"; .;
-      hence "x <= Union c"; by fast;
-      also; have [RS sym]: "graph H h = Union c"; .;
-      finally; show ?thesis; .;
-    qed;
-  qed;
-qed;
+    thus ?thesis 
+    proof (elim exE conjE) 
+      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" .
+      finally show ?thesis .
+    qed
+  qed
+qed
 
 text{* \medskip The domain $H$ of the limit function is a superspace of $F$,
 since $F$ is a subset of $H$. The existence of the $\zero$ element in
 $F$ and the closure properties follow from the fact that $F$ is a
-vector space. *};
+vector space. *}
 
 lemma sup_supF: 
-  "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c;
+  "[| 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 |] 
-  ==> is_subspace F H";
-proof -; 
-  assume "M = norm_pres_extensions E p F f" "c: chain M" "EX x. x:c"
-    "graph H h = Union 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"
 
-  show ?thesis; 
-  proof;
-    show "\<zero> : F"; ..;
-    show "F <= H"; 
-    proof (rule graph_extD2);
-      show "graph F f <= graph H h";
-        by (rule sup_ext);
-    qed;
-    show "ALL x:F. ALL y:F. x + y : F"; 
-    proof (intro ballI); 
-      fix x y; assume "x:F" "y:F";
-      show "x + y : F"; by (simp!);
-    qed;
-    show "ALL x:F. ALL a. a \<prod> x : F";
-    proof (intro ballI allI);
-      fix x a; assume "x:F";
-      show "a \<prod> x : F"; by (simp!);
-    qed;
-  qed;
-qed;
+  show ?thesis 
+  proof
+    show "\<zero> \<in> F" ..
+    show "F \\<subseteq> H" 
+    proof (rule graph_extD2)
+      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" 
+    proof (intro ballI) 
+      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"
+    proof (intro ballI allI)
+      fix x a assume "x\<in>F"
+      show "a \<prod> x \<in> F" by (simp!)
+    qed
+  qed
+qed
 
 text{* \medskip The domain $H$ of the limit function is a subspace
-of $E$. *};
+of $E$. *}
 
 lemma sup_subE: 
-  "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c; 
+  "[| 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 |] 
-  ==> is_subspace H E";
-proof -; 
-  assume "M = norm_pres_extensions E p F f" "c: chain M" "EX x. x:c"
-    "graph H h = Union c" "is_subspace F E" "is_vectorspace E";
-  show ?thesis; 
-  proof;
+  ==> 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"
+  show ?thesis 
+  proof
  
     txt {* The $\zero$ element is in $H$, as $F$ is a subset 
-    of $H$: *};
+    of $H$: *}
 
-    have "\<zero> : F"; ..;
-    also; have "is_subspace F H"; by (rule sup_supF); 
-    hence "F <= H"; ..;
-    finally; show "\<zero> : H"; .;
+    have "\<zero> \<in> F" ..
+    also have "is_subspace F H" by (rule sup_supF) 
+    hence "F \\<subseteq> H" ..
+    finally show "\<zero> \<in> H" .
 
-    txt{* $H$ is a subset of $E$: *};
+    txt{* $H$ is a subset of $E$: *}
 
-    show "H <= E"; 
-    proof;
-      fix x; assume "x:H";
-      have "EX H' h'. x:H' & graph H' h' <= graph H h
+    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 <= graph H' h' 
-              & (ALL x:H'. h' x <= p x)"; 
-	by (rule some_H'h');
-      thus "x:E"; 
-      proof (elim exE conjE);
-	fix H' h'; assume "x:H'" "is_subspace H' E";
-        have "H' <= E"; ..;
-	thus "x:E"; ..;
-      qed;
-    qed;
+              & is_subspace F H' & graph F f \\<subseteq> graph H' h' 
+              & (\<forall> x\<in>H'. h' x \\<le> p x)" 
+	by (rule some_H'h')
+      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" ..
+      qed
+    qed
 
-    txt{* $H$ is closed under addition: *};
+    txt{* $H$ is closed under addition: *}
 
-    show "ALL x:H. ALL y:H. x + y : H"; 
-    proof (intro ballI); 
-      fix x y; assume "x:H" "y:H";
-      have "EX H' h'. x:H' & y:H' & graph H' h' <= graph H 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 <= graph H' h' 
-              & (ALL x:H'. h' x <= p x)"; 
-	by (rule some_H'h'2); 
-      thus "x + y : H"; 
-      proof (elim exE conjE); 
-	fix H' h'; 
-        assume "x:H'" "y:H'" "is_subspace H' E" 
-          "graph H' h' <= graph H h";
-        have "x + y : H'"; ..;
-	also; have "H' <= H"; ..;
-	finally; show ?thesis; .;
-      qed;
-    qed;      
+              & is_subspace F H' & graph F f \\<subseteq> graph H' h' 
+              & (\<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"
+        have "x + y \<in> H'" ..
+	also have "H' \\<subseteq> H" ..
+	finally show ?thesis .
+      qed
+    qed      
 
-    txt{* $H$ is closed under scalar multiplication: *};
+    txt{* $H$ is closed under scalar multiplication: *}
 
-    show "ALL x:H. ALL a. a \<prod> x : H"; 
-    proof (intro ballI allI); 
-      fix x a; assume "x:H"; 
-      have "EX H' h'. x:H' & graph H' h' <= graph H h
+    show "\<forall> x\<in>H. \<forall> a. a \<prod> 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 <= graph H' h' 
-              & (ALL x:H'. h' x <= p x)"; 
-	by (rule some_H'h'); 
-      thus "a \<prod> x : H"; 
-      proof (elim exE conjE);
-	fix H' h'; 
-        assume "x:H'" "is_subspace H' E" "graph H' h' <= graph H h";
-        have "a \<prod> x : H'"; ..;
-        also; have "H' <= H"; ..;
-	finally; show ?thesis; .;
-      qed;
-    qed;
-  qed;
-qed;
+              & is_subspace F H' & graph F f \\<subseteq> graph H' h' 
+              & (\<forall> x\<in>H'. h' x \\<le> p x)" 
+	by (rule some_H'h') 
+      thus "a \<prod> 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" ..
+	finally show ?thesis .
+      qed
+    qed
+  qed
+qed
 
 text {* \medskip The limit function is bounded by 
 the norm $p$ as well, since all elements in the chain are
 bounded by $p$.
-*};
+*}
 
-lemma sup_norm_pres: 
-  "[| M = norm_pres_extensions E p F f; c: chain M; 
-  graph H h = Union c |] ==> ALL x:H. h x <= p x";
-proof;
-  assume "M = norm_pres_extensions E p F f" "c: chain M" 
-         "graph H h = Union c";
-  fix x; assume "x:H";
-  have "EX H' h'. x:H' & graph H' h' <= graph H h 
+lemma sup_norm_pres:
+  "[| 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"
+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 <= graph H' h' & (ALL x:H'. h' x <= p x)"; 
-    by (rule some_H'h');
-  thus "h x <= p x"; 
-  proof (elim exE conjE);
-    fix H' h'; 
-    assume "x: H'" "graph H' h' <= graph H h" 
-      and a: "ALL x: H'. h' x <= p x";
-    have [RS sym]: "h' x = h x"; ..;
-    also; from a; have "h' x <= p x "; ..;
-    finally; show ?thesis; .;  
-  qed;
-qed;
+          & graph F f \\<subseteq> graph H' h' & (\<forall> x\<in>H'. h' x \\<le> p x)" 
+    by (rule some_H'h')
+  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"
+    have [RS sym]: "h' x = h x" ..
+    also from a have "h' x \\<le> p x " ..
+    finally show ?thesis .  
+  qed
+qed
 
 
 text{* \medskip The following lemma is a property of linear forms on 
@@ -644,47 +494,47 @@
 \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}
-*};
+*}
 
 lemma abs_ineq_iff: 
   "[| is_subspace H E; is_vectorspace E; is_seminorm E p; 
   is_linearform H h |] 
-  ==> (ALL x:H. abs (h x) <= p x) = (ALL x:H. h x <= p x)" 
-  (concl is "?L = ?R");
-proof -;
+  ==> (\<forall> x\<in>H. abs (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" 
-         "is_linearform H h";
-  have h: "is_vectorspace H"; ..;
-  show ?thesis;
-  proof; 
-    assume l: ?L;
-    show ?R;
-    proof;
-      fix x; assume x: "x:H";
-      have "h x <= abs (h x)"; by (rule abs_ge_self);
-      also; from l; have "... <= p x"; ..;
-      finally; show "h x <= p x"; .;
-    qed;
-  next;
-    assume r: ?R;
-    show ?L;
-    proof; 
-      fix x; assume "x:H";
-      show "!! a b :: real. [| - a <= b; b <= a |] ==> abs b <= a";
-        by arith;
-      show "- p x <= h x";
-      proof (rule real_minus_le);
-	from h; have "- h x = h (- x)"; 
-          by (rule linearform_neg [RS sym]);
-	also; from r; have "... <= p (- x)"; by (simp!);
-	also; have "... = p x"; 
-          by (rule seminorm_minus [OF _ subspace_subsetD]);
-	finally; show "- h x <= p x"; .; 
-      qed;
-      from r; show "h x <= p x"; ..; 
-    qed;
-  qed;
-qed;  
+         "is_linearform H h"
+  have h: "is_vectorspace H" ..
+  show ?thesis
+  proof 
+    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" .
+    qed
+  next
+    assume r: ?R
+    show ?L
+    proof 
+      fix x assume "x\<in>H"
+      show "!! a b :: real. [| - a \\<le> b; b \\<le> a |] ==> abs b \\<le> a"
+        by arith
+      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 have "... = p x" 
+          by (rule seminorm_minus [OF _ subspace_subsetD])
+	finally show "- h x \\<le> p x" . 
+      qed
+      from r show "h x \\<le> p x" .. 
+    qed
+  qed
+qed  
 
 
-end;
\ No newline at end of file
+end
\ No newline at end of file