# HG changeset patch
# User bauerg
# Date 962871010 -7200
# Node ID f9a6670427fb352f0a2f260e6d8350033c8367fe
# Parent  2ceb11a2e190a6ea927359b4f65aa6a27ca1c0eb
completed TYPES version of HahnBanach;

diff -r 2ceb11a2e190 -r f9a6670427fb src/HOL/Real/HahnBanach/Aux.thy
--- a/src/HOL/Real/HahnBanach/Aux.thy	Thu Jul 06 09:46:56 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Aux.thy	Thu Jul 06 10:10:10 2000 +0200
@@ -59,15 +59,14 @@
 lemma abs_minus_one: "abs (- (#1::real)) = #1" 
   by simp
 
-
 lemma real_mult_le_le_mono1a: 
   "[| (#0::real) <= z; x <= y |] ==> z * x  <= z * y"
 proof -
-  assume "(#0::real) <= z" "x <= y"
+  assume z: "(#0::real) <= z" and "x <= y"
   hence "x < y | x = y" by (force simp add: order_le_less)
   thus ?thesis
   proof (elim disjE) 
-   assume "x < y" show ?thesis by (rule real_mult_le_less_mono2) simp
+   assume "x < y" show ?thesis by  (rule real_mult_le_less_mono2) simp
   next 
    assume "x = y" thus ?thesis by simp
   qed
diff -r 2ceb11a2e190 -r f9a6670427fb src/HOL/Real/HahnBanach/HahnBanach.thy
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Jul 06 09:46:56 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Jul 06 10:10:10 2000 +0200
@@ -1,59 +1,23 @@
-(*  Title:      HOL/Real/HahnBanach/HahnBanach.thy
-    ID:         $Id$
-    Author:     Gertrud Bauer, TU Munich
-*)
-
-header {* The Hahn-Banach Theorem *}
-
-theory HahnBanach
-     = HahnBanachSupLemmas + HahnBanachExtLemmas + ZornLemma:
-
-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 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$.
+theory HahnBanach = HahnBanachLemmas: text_raw {* \smallskip\\ *} (* from ~/Pub/TYPES99/HB/HahnBanach.thy *)
 
- \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; is_subspace F E; 
- is_seminorm E p; is_linearform F f; ALL x:F. f x <= p x |]
-  ==> EX h. is_linearform E h & (ALL x:F. h x = f x)
-          & (ALL x:E. h x <= p x)"
+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)"   
+    -- {* 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 -
-
-txt {* 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$. *}
-
   assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p" 
-    "is_linearform F f" "ALL x:F. f x <= p x"
-
-txt {* Define $M$ as the set of all norm-preserving extensions of $F$.  *}
-
+   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 : chain M" "EX x. x:c"
-
-txt {* Show that every non-empty chain $c$ in $M$ has an upper bound in $M$: $\Union c$ is greater that every element of the chain $c$, so $\Union c$ is an upper bound of $c$ that lies in $M$. *}
-
-    have "Union c : M"
+    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$. *}
     proof (unfold M_def, rule norm_pres_extensionI)
       show "EX (H::'a set) h::'a => real. graph H h = Union c
               & is_linearform H h 
@@ -72,21 +36,24 @@
         qed
         show "is_linearform ?H ?h" 
           by (simp! add: sup_lf a)
-        show "is_subspace ?H E"
-          by (rule sup_subE [OF _ _ _ a]) (simp!)+
+        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 F ?H" 
           by (rule sup_supF [OF _ _ _ a]) (simp!)+
+  (* FIXME        by (rule sup_supF, rule a) (simp!)+ *)
         show "graph F f <= 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" 
           by (rule sup_norm_pres [OF _ _ a]) (simp!)+
+  (* FIXME        by (rule sup_norm_pres, rule a) (simp!)+ *)
       qed
     qed
+
   }
-  
-txt {* With Zorn's Lemma we can conclude that there is a maximal element $g$ in $M$. *}
-
-  hence "EX g:M. ALL x:M. g <= x --> g = x"
+  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 *}
   proof (rule Zorn's_Lemma)
     txt {* We show that $M$ is non-empty: *}
     have "graph F f : norm_pres_extensions E p F f"
@@ -98,20 +65,15 @@
   qed
   thus ?thesis
   proof
-
-txt {* We take this maximal element $g$.  *}
-
-    fix g assume "g:M" "ALL x:M. g <= x --> g = x"
+    fix g assume "g \\<in> M" "\\<forall>x \\<in> M. g \\<subseteq> x \\<longrightarrow> g = x"
+    -- {* We consider such a maximal element $g \in M$. \skp *}
     show ?thesis
-
-      txt {* $g$ is a norm-preserving extension of $f$, that is: $g$
-      is the graph of a linear form $h$, defined on a subspace $H$ of
-      $E$, which is a superspace of $F$. $h$ is an extension of $f$
-      and $h$ is again bounded by $p$. *}
-
       obtain H h where "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"
+        "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 *}
       proof -
         have "EX H h. graph H h = g & is_linearform H h 
           & is_subspace H E & is_subspace F H
@@ -120,144 +82,100 @@
         thus ?thesis by (elim exE conjE) rule
       qed
       have h: "is_vectorspace H" ..
-
-txt {* We show that $h$ is defined on whole $E$ by classical contradiction.  *} 
-
-      have "H = E" 
+      have "H = E"
+      -- {* We show that $h$ is defined on whole $E$ by classical contradiction. \skp *} 
       proof (rule classical)
-
-	txt {* Assume $h$ is not defined on whole $E$. *}
-
-        assume "H ~= E"
-
-txt {* Then show that $h$ can be extended in a norm-preserving way to a function $h_0$ with the graph $g_{h0}$.  *}
-
-        have "EX g_h0 : M. g <= g_h0 & g ~= g_h0" 
-
-	  txt {* Consider $x_0 \in E \setminus H$. *}
-
-          obtain x0 where "x0:E" "x0~:H" 
+        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 *}
           proof -
-            have "EX x0:E. x0~:H"
+            have "EX x':E. x'~:H"
             proof (rule set_less_imp_diff_not_empty)
               have "H <= E" ..
               thus "H < E" ..
             qed
             thus ?thesis by blast
           qed
-          have x0: "x0 ~= 00"
+          have x': "x' ~= \<zero>"
           proof (rule classical)
-            presume "x0 = 00"
-            with h have "x0:H" by simp
+            presume "x' = \<zero>"
+            with h have "x':H" by simp
             thus ?thesis by contradiction
           qed blast
-
-txt {* Define $H_0$ as the direct sum of $H$ and the linear closure of $x_0$.  *}
-
-          def H0 == "H + lin x0"
+          def H' == "H + lin x'"
+          -- {* Define $H'$ as the direct sum of $H$ and the linear closure of $x'$. \skp *}
           show ?thesis
-
-	    txt {* Pick a real number $\xi$ that fulfills certain
-	    inequations, which will be used to establish that $h_0$ is
-	    a norm-preserving extension of $h$. *}
-
-            obtain xi where "ALL y:H. - p (y + x0) - h y <= xi 
-                              & xi <= p (y + x0) - h y"
-            proof -
-	      from h have "EX xi. ALL y:H. - p (y + x0) - h y <= xi 
-                              & xi <= p (y + x0) - 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 = x0 + - x0 + v + - u"
-                  by (simp! add: diff_eq1)
-                also have "... = v + x0 + - (u + x0)"
-                  by (simp!)
-                also have "... = (v + x0) - (u + x0)"
-                  by (simp! add: diff_eq1)
-                also have "p ... <= p (v + x0) + p (u + x0)"
-                  by (rule seminorm_diff_subadditive) (simp!)+
-                finally have "h v - h u <= p (v + x0) + p (u + x0)" .
-
-                thus "- p (u + x0) - h u <= p (v + x0) - h v"
-                  by (rule real_diff_ineq_swap)
-              qed
-              thus ?thesis by rule rule
-            qed
-
-txt {* Define the extension $h_0$ of $h$ to $H_0$ using $\xi$.  *}
-
-            def h0 == "\\<lambda>x. let (y,a) = SOME (y, a). x = y + a (*) x0 
-                                                  & y:H
+            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 *}
+            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 *}
             show ?thesis
             proof
- 
-txt {* Show that $h_0$ is an extension of $h$  *}
- 
-              show "g <= graph H0 h0 & g ~= graph H0 h0"
-              proof
-		show "g <= graph H0 h0"
+              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'"
 		proof -
-		  have  "graph H h <= graph H0 h0"
+		  have  "graph H h <= graph H' h'"
                   proof (rule graph_extI)
 		    fix t assume "t:H" 
-		    have "(SOME (y, a). t = y + a (*) x0 & y : H)
-                         = (t,#0)"
-		      by (rule decomp_H0_H [OF _ _ _ _ _ x0])
-		    thus "h t = h0 t" by (simp! add: Let_def)
+		    have "(SOME (y, a). t = y + a \<prod> x' & y : H)
+                         = (t, #0)" 
+		      by (rule decomp_H0_H [OF _ _ _ _ _ x'])
+		    thus "h t = h' t" by (simp! add: Let_def)
 		  next
-		    show "H <= H0"
+		    show "H <= H'"
 		    proof (rule subspace_subset)
-		      show "is_subspace H H0"
-		      proof (unfold H0_def, rule subspace_vs_sum1)
+		      show "is_subspace H H'"
+		      proof (unfold H'_def, rule subspace_vs_sum1)
 			show "is_vectorspace H" ..
-			show "is_vectorspace (lin x0)" ..
+			show "is_vectorspace (lin x')" ..
 		      qed
 		    qed
 		  qed 
 		  thus ?thesis by (simp!)
 		qed
-                show "g ~= graph H0 h0"
+                show "g ~= graph H' h'"
 		proof -
-		  have "graph H h ~= graph H0 h0"
+		  have "graph H h ~= graph H' h'"
 		  proof
-		    assume e: "graph H h = graph H0 h0"
-		    have "x0 : H0" 
-		    proof (unfold H0_def, rule vs_sumI)
-		      show "x0 = 00 + x0" by (simp!)
-		      from h show "00 : H" ..
-		      show "x0 : lin x0" by (rule x_lin_x)
+		    assume e: "graph H h = graph H' h'"
+		    have "x' : 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)
 		    qed
-		    hence "(x0, h0 x0) : graph H0 h0" ..
-		    with e have "(x0, h0 x0) : graph H h" by simp
-		    hence "x0 : H" ..
+		    hence "(x', h' x') : graph H' h'" ..
+		    with e have "(x', h' x') : graph H h" by simp
+		    hence "x' : H" ..
 		    thus False by contradiction
 		  qed
 		  thus ?thesis by (simp!)
 		qed
               qed
-	      
-txt {* and $h_0$ is norm-preserving.  *} 
-
-              show "graph H0 h0 : M"
-	      proof -
-		have "graph H0 h0 : norm_pres_extensions E p F f"
+	      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"
 		proof (rule norm_pres_extensionI2)
-		  show "is_linearform H0 h0"
-		    by (rule h0_lf [OF _ _ _ _ _ _ x0]) (simp!)+
-		  show "is_subspace H0 E"
-		    by (unfold H0_def) (rule vs_sum_subspace [OF _ lin_subspace])
+		  show "is_linearform H' h'"
+		    by (rule h0_lf [OF _ _ _ _ _ _ x']) (simp!)+
+		  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 
-		  have [fold H0_def]: "is_subspace H (H + lin x0)" ..
+		  have [fold H'_def]: "is_subspace H (H + lin x')" ..
 		  finally (subspace_trans [OF _ h]) 
-		  show f_h0: "is_subspace F H0" .
+		  show f_h': "is_subspace F H'" .
 		
-		  show "graph F f <= graph H0 h0"
+		  show "graph F f <= graph H' h'"
 		  proof (rule graph_extI)
 		    fix x assume "x:F"
 		    have "f x = h x" ..
@@ -265,37 +183,31 @@
 		    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 (*) x0 & y : H)"
-		      by (rule decomp_H0_H [RS sym, OF _ _ _ _ _ x0]) (simp!)+
+		      "(x, #0) = (SOME (y, a). x = y + a (*) x' & y : H)"
+		      by (rule decomp_H0_H [RS sym, OF _ _ _ _ _ x']) (simp!)+
 		    also have 
-		      "(let (y,a) = (SOME (y,a). x = y + a (*) x0 & y : H)
+		      "(let (y,a) = (SOME (y,a). x = y + a (*) x' & y : H)
                         in h y + a * xi) 
-                      = h0 x" by (simp!)
-		    finally show "f x = h0 x" .
+                      = h' x" by (simp!)
+		    finally show "f x = h' x" .
 		  next
-		    from f_h0 show "F <= H0" ..
+		    from f_h' show "F <= H'" ..
 		  qed
 		
-		  show "ALL x:H0. h0 x <= p x"
-		    by (rule h0_norm_pres [OF _ _ _ _ x0])
+		  show "ALL x:H'. h' x <= p x"
+		    by (rule h0_norm_pres [OF _ _ _ _ x'])
 		qed
-		thus "graph H0 h0 : M" by (simp!)
+		thus "graph H' h' : M" by (simp!)
 	      qed
             qed
           qed
         qed
-
-txt {* So the graph $g$ of $h$ cannot be maximal. Contradiction.  *} 
-
-        hence "~ (ALL x:M. g <= x --> g = x)" by simp
-        thus ?thesis by contradiction
-      qed 
-
-txt {* Now we have a linear extension $h$ of $f$ to $E$ that is 
-bounded by $p$. *}
-
-      thus "EX h. is_linearform E h & (ALL x:F. h x = f x) 
-                & (ALL x:E. h x <= p x)"
+        hence "\\<not>(\\<forall>x \\<in> M. g \\<subseteq> x \\<longrightarrow> 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)" 
       proof (intro exI conjI)
         assume eq: "H = E"
 	from eq show "is_linearform E h" by (simp!)
@@ -307,498 +219,5 @@
       qed
     qed
   qed
-qed
-(*
-theorem HahnBanach: 
-  "[| is_vectorspace E; is_subspace F E; is_seminorm E p; 
-  is_linearform F f; ALL x:F. f x <= p x |]
-  ==> EX h. is_linearform E h
-          & (ALL x:F. h x = f x)
-          & (ALL x:E. h x <= p x)";
-proof -;
-  assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p"
-         "is_linearform F f" "ALL x:F. f x <= p x";
-  
-  txt{* We define $M$ to be the set of all linear extensions 
-  of $f$ to superspaces of $F$, which are bounded by $p$. *}
-
-  def M == "norm_pres_extensions E p F f"
-  
-  txt{* We show that $M$ is non-empty: *}
- 
-  have aM: "graph F f : norm_pres_extensions E p F f"
-  proof (rule norm_pres_extensionI2)
-    have "is_vectorspace F" ..
-    thus "is_subspace F F" ..
-  qed (blast!)+
-
-  subsubsect {* Existence of a limit function *} 
-
-  txt {* For every non-empty chain of norm-preserving extensions
-  the union of all functions in the chain is again a norm-preserving
-  extension. (The union is an upper bound for all elements. 
-  It is even the least upper bound, because every upper bound of $M$
-  is also an upper bound for $\Union c$, as $\Union c\in M$) *}
-
-  {
-    fix c assume "c:chain M" "EX x. x:c"
-    have "Union c : M"
-
-    proof (unfold M_def, rule norm_pres_extensionI)
-      show "EX (H::'a set) h::'a => real. 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)"
-      proof (intro exI conjI)
-        let ?H = "domain (Union c)"
-        let ?h = "funct (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"
-          show "z = y" by (rule sup_definite)
-        qed
-        show "is_linearform ?H ?h"  
-          by (simp! add: sup_lf a)
-        show "is_subspace ?H E" 
-          by (rule sup_subE, rule a) (simp!)+
-        show "is_subspace F ?H" 
-          by (rule sup_supF, rule a) (simp!)+
-        show "graph F f <= graph ?H ?h" 
-          by (rule sup_ext, rule a) (simp!)+
-        show "ALL x::'a:?H. ?h x <= p x" 
-          by (rule sup_norm_pres, rule a) (simp!)+
-      qed
-    qed
-  }
- 
-  txt {* According to Zorn's Lemma there is
-  a maximal norm-preserving extension $g\in M$. *}
-  
-  with aM have bex_g: "EX g:M. ALL x:M. g <= x --> g = x"
-    by (simp! add: Zorn's_Lemma)
-
-  thus ?thesis
-  proof
-    fix g assume g: "g:M" "ALL x:M. g <= x --> g = x"
- 
-    have ex_Hh: 
-      "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 (simp! add: norm_pres_extension_D)
-    thus ?thesis
-    proof (elim exE conjE, intro exI)
-      fix H h 
-      assume "graph H h = g" "is_linearform (H::'a set) h" 
-             "is_subspace H E" "is_subspace F H"
-        and h_ext: "graph F f <= graph H h"
-        and h_bound: "ALL x:H. h x <= p x"
-
-      have h: "is_vectorspace H" ..
-      have f: "is_vectorspace F" ..
-
-subsubsect {* The domain of the limit function *}
-
-have eq: "H = E" 
-proof (rule classical)
-
-txt {* Assume that the domain of the supremum is not $E$, *}
-
-  assume "H ~= E"
-  have "H <= E" ..
-  hence "H < E" ..
- 
-  txt{* then there exists an element $x_0$ in $E \setminus H$: *}
-
-  hence "EX x0:E. x0~:H" 
-    by (rule set_less_imp_diff_not_empty)
-
-  txt {* We get that $h$ can be extended  in a 
-  norm-preserving way to some $H_0$. *}
-
-  hence "EX H0 h0. g <= graph H0 h0 & g ~= graph H0 h0 
-                 & graph H0 h0 : M"
-  proof
-    fix x0 assume "x0:E" "x0~:H"
-
-    have x0: "x0 ~= 00"
-    proof (rule classical)
-      presume "x0 = 00"
-      with h have "x0:H" by simp
-      thus ?thesis by contradiction
-    qed blast
-
-    txt {* Define $H_0$ as the (direct) sum of H and the 
-    linear closure of $x_0$. \label{ex-xi-use}*}
-
-    def H0 == "H + lin x0"
-
-    from h have xi: "EX xi. ALL y:H. - p (y + x0) - h y <= xi 
-                                    & xi <= p (y + x0) - 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 from h_bound have "... <= p (v - u)"
-        by (simp!)
-      also have "v - u = x0 + - x0 + v + - u"
-        by (simp! add: diff_eq1)
-      also have "... = v + x0 + - (u + x0)"
-        by (simp!)
-      also have "... = (v + x0) - (u + x0)"
-        by (simp! add: diff_eq1)
-      also have "p ... <= p (v + x0) + p (u + x0)"
-         by (rule seminorm_diff_subadditive) (simp!)+
-      finally have "h v - h u <= p (v + x0) + p (u + x0)" .
-
-      thus "- p (u + x0) - h u <= p (v + x0) - h v"
-        by (rule real_diff_ineq_swap)
-    qed
-    hence "EX h0. g <= graph H0 h0 & g ~= graph H0 h0
-               & graph H0 h0 : M" 
-    proof (elim exE, intro exI conjI)
-      fix xi 
-      assume a: "ALL y:H. - p (y + x0) - h y <= xi 
-                        & xi <= p (y + x0) - h y"
-     
-      txt {* Define $h_0$ as the canonical linear extension 
-      of $h$ on $H_0$:*}  
-
-      def h0 ==
-          "\\<lambda>x. let (y,a) = SOME (y, a). x = y + a ( * ) x0 & y:H
-               in (h y) + a * xi"
-
-      txt {* We get that the graph of $h_0$ extends that of
-      $h$. *}
-        
-      have  "graph H h <= graph H0 h0" 
-      proof (rule graph_extI)
-        fix t assume "t:H" 
-        have "(SOME (y, a). t = y + a ( * ) x0 & y : H) = (t,#0)"
-          by (rule decomp_H0_H, rule x0) 
-        thus "h t = h0 t" by (simp! add: Let_def)
-      next
-        show "H <= H0"
-        proof (rule subspace_subset)
-	  show "is_subspace H H0"
-          proof (unfold H0_def, rule subspace_vs_sum1)
-       	    show "is_vectorspace H" ..
-            show "is_vectorspace (lin x0)" ..
-          qed
-        qed
-      qed
-      thus "g <= graph H0 h0" by (simp!)
-
-      txt {* Apparently $h_0$ is not equal to $h$. *}
-
-      have "graph H h ~= graph H0 h0"
-      proof
-        assume e: "graph H h = graph H0 h0"
-        have "x0 : H0" 
-        proof (unfold H0_def, rule vs_sumI)
-          show "x0 = 00 + x0" by (simp!)
-          from h show "00 : H" ..
-          show "x0 : lin x0" by (rule x_lin_x)
-        qed
-        hence "(x0, h0 x0) : graph H0 h0" ..
-        with e have "(x0, h0 x0) : graph H h" by simp
-        hence "x0 : H" ..
-        thus False by contradiction
-      qed
-      thus "g ~= graph H0 h0" by (simp!)
-
-      txt {* Furthermore  $h_0$ is a norm-preserving extension 
-     of $f$. *}
-
-      have "graph H0 h0 : norm_pres_extensions E p F f"
-      proof (rule norm_pres_extensionI2)
-        show "is_linearform H0 h0"
-          by (rule h0_lf, rule x0) (simp!)+
-        show "is_subspace H0 E"
-          by (unfold H0_def, rule vs_sum_subspace, 
-             rule lin_subspace)
-
-        have "is_subspace F H" .
-        also from h lin_vs 
-	have [fold H0_def]: "is_subspace H (H + lin x0)" ..
-        finally (subspace_trans [OF _ h]) 
-	show f_h0: "is_subspace F H0" . (*** 
-        backwards:
-        show f_h0: "is_subspace F H0"; .;
-        proof (rule subspace_trans [of F H H0]);
-          from h lin_vs; 
-          have "is_subspace H (H + lin x0)"; ..;
-          thus "is_subspace H H0"; by (unfold H0_def);
-        qed; ***)
-
-        show "graph F f <= graph H0 h0"
-        proof (rule graph_extI)
-          fix x assume "x: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 ( * ) x0 & y : H)"
-            by (rule decomp_H0_H [RS sym], rule x0) (simp!)+
-          also have 
-            "(let (y,a) = (SOME (y,a). x = y + a ( * ) x0 & y : H)
-              in h y + a * xi) 
-             = h0 x" by (simp!)
-          finally show "f x = h0 x" .
-        next
-          from f_h0 show "F <= H0" ..
-        qed
-
-        show "ALL x:H0. h0 x <= p x"
-          by (rule h0_norm_pres, rule x0) (assumption | simp!)+
-      qed
-      thus "graph H0 h0 : M" by (simp!)
-    qed
-    thus ?thesis ..
-  qed
-
-  txt {* We have shown that $h$ can still be extended to 
-  some $h_0$, in contradiction to the assumption that 
-  $h$ is a maximal element. *}
-
-  hence "EX x:M. g <= x & g ~= x" 
-    by (elim exE conjE, intro bexI conjI)
-  hence "~ (ALL x:M. g <= x --> g = x)" by simp
-  thus ?thesis by contradiction
-qed 
-
-txt{* It follows $H = E$, and the thesis can be shown. *}
-
-show "is_linearform E h & (ALL x:F. h x = f x) 
-     & (ALL x:E. h x <= p x)"
-proof (intro conjI) 
-  from eq show "is_linearform E h" by (simp!)
-  show "ALL x:F. h x = f x" 
-  proof (intro ballI, rule sym)
-    fix x assume "x:F" show "f x = h x " ..
-  qed
-  from eq show "ALL x:E. h x <= p x" by (force!)
-qed
-
-qed
-qed
-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; ALL x:F. abs (f x) <= p x |]
-  ==> EX g. is_linearform E g & (ALL x:F. g x = f x)
-   & (ALL x:E. abs (g x) <= p x)"
-proof -
-  assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p" 
-    "is_linearform F f"  "ALL x:F. abs (f x) <= p x"
-  have "ALL x:F. f x <= p x"  by (rule abs_ineq_iff [RS iffD1])
-  hence "EX g. is_linearform E g & (ALL x:F. g x = f x) 
-              & (ALL x:E. g x <= p x)"
-    by (simp! only: HahnBanach)
-  thus ?thesis 
-  proof (elim exE conjE)
-    fix g assume "is_linearform E g" "ALL x:F. g x = f x" 
-                  "ALL x:E. g x <= p x"
-    hence "ALL x:E. abs (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 |] 
-  ==> EX g. is_linearform E g
-         & is_continuous E norm g 
-         & (ALL x:F. g x = f x) 
-         & function_norm E norm g = function_norm F norm f"
-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" ..
-  with _ have 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. function_norm F norm f * norm x"
-  
-  txt{* $p$ is a seminorm on $E$: *}
-
-  have q: "is_seminorm E p"
-  proof
-    fix x y a assume "x:E" "y:E"
-
-    txt{* $p$ is positive definite: *}
-
-    show "#0 <= p x"
-    proof (unfold p_def, rule real_le_mult_order1a)
-      from _ f_norm show "#0 <= function_norm F norm f" ..
-      show "#0 <= norm x" ..
-    qed
-
-    txt{* $p$ is absolutely homogenous: *}
-
-    show "p (a (*) x) = abs a * p x"
-    proof - 
-      have "p (a (*) x) = function_norm F norm f * norm (a (*) x)"
-        by (simp!)
-      also have "norm (a (*) x) = abs a * norm x" 
-        by (rule normed_vs_norm_abs_homogenous)
-      also have "function_norm F norm f * (abs a * norm x) 
-        = abs a * (function_norm F norm f * norm x)"
-        by (simp! only: real_mult_left_commute)
-      also have "... = abs 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) = function_norm F norm f * norm (x + y)"
-        by (simp!)
-      also 
-      have "... <= function_norm F norm f * (norm x + norm y)"
-      proof (rule real_mult_le_le_mono1a)
-        from _ f_norm show "#0 <= function_norm F norm f" ..
-        show "norm (x + y) <= norm x + norm y" ..
-      qed
-      also have "... = function_norm F norm f * norm x 
-                        + function_norm F norm f * norm y"
-        by (simp! only: real_add_mult_distrib2)
-      finally show ?thesis by (simp!)
-    qed
-  qed
-
-  txt{* $f$ is bounded by $p$. *} 
-
-  have "ALL x:F. abs (f x) <= p x"
-  proof
-    fix x assume "x:F"
-     from f_norm show "abs (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 "EX g. is_linearform E g & (ALL x:F. g x = f x) 
-            & (ALL x:E. abs (g x) <= p x)"
-    by (simp! add: abs_HahnBanach)
-
-  thus ?thesis
-  proof (elim exE conjE) 
-    fix g
-    assume "is_linearform E g" and a: "ALL x:F. g x = f x" 
-       and b: "ALL x:E. abs (g x) <= p x"
-
-    show "EX g. is_linearform E g 
-            & is_continuous E norm g 
-            & (ALL x:F. g x = f x) 
-            & function_norm E norm g = function_norm F norm f"
-    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:E"
-        from b [RS bspec, OF this] 
-        show "abs (g x) <= function_norm F norm f * norm x"
-          by (unfold p_def)
-      qed 
-
-      txt {* To complete the proof, we show that 
-      $\fnorm g = \fnorm f$. \label{order_antisym} *}
-
-      show "function_norm E norm g = function_norm F norm f"
-        (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 "ALL x:E. abs (g x) <= function_norm F norm f * norm x"
-        proof
-          fix x assume "x:E" 
-          show "abs (g x) <= function_norm F norm f * norm x"
-            by (simp!)
-        qed
-
-        with _ g_cont show "?L <= ?R"
-        proof (rule fnorm_le_ub)
-          from f_cont f_norm show "#0 <= function_norm F norm f" ..
-        qed
-
-        txt{* The other direction is achieved by a similar 
-        argument. *}
-
-        have "ALL x:F. abs (f x) <= function_norm E norm g * norm x"
-        proof
-          fix x assume "x : F" 
-          from a have "g x = f x" ..
-          hence "abs (f x) = abs (g x)" by simp
-          also from _ _ g_cont
-          have "... <= function_norm E norm g * norm x"
-          proof (rule norm_fx_le_norm_f_norm_x)
-            show "x:E" ..
-          qed
-          finally show "abs (f x) <= function_norm E norm g * norm x" .
-        qed 
-        thus "?R <= ?L" 
-        proof (rule fnorm_le_ub [OF f_norm f_cont])
-          from g_cont show "#0 <= function_norm E norm g" ..
-        qed
-      qed
-    qed
-  qed
-qed
-
+qed text_raw {* \smallskip\\ *}
 end
\ No newline at end of file
diff -r 2ceb11a2e190 -r f9a6670427fb src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Thu Jul 06 09:46:56 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Thu Jul 06 10:10:10 2000 +0200
@@ -3,9 +3,9 @@
     Author:     Gertrud Bauer, TU Munich
 *)
 
-header {* Extending non-maximal functions *}
+header {* Extending non-maximal functions *};
 
-theory HahnBanachExtLemmas = FunctionNorm:
+theory HahnBanachExtLemmas = FunctionNorm:;
 
 text{* In this section the following context is presumed.
 Let $E$ be a real vector space with a 
@@ -19,7 +19,7 @@
 $h_0\ap x = h\ap y + a \cdot \xi$ for a certain $\xi$.
 
 Subsequently we show some properties of this extension $h_0$ of $h$.
-*} 
+*}; 
 
 
 text {* This lemma will be used to show the existence of a linear
@@ -32,318 +32,318 @@
 it suffices to show that 
 \begin{matharray}{l} \All
 {u\in F}{\All {v\in F}{a\ap u \leq b \ap v}} 
-\end{matharray} *}
+\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" 
-proof -
-  assume vs: "is_vectorspace F"
-  assume r: "(!! u v. [| u:F; v:F |] ==> a u <= (b v::real))"
+  ==> EX (xi::real). ALL y:F. a y <= xi & xi <= b y"; 
+proof -;
+  assume vs: "is_vectorspace F";
+  assume r: "(!! u v. [| u:F; v: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. *}
+  it is non-empty and has an upper bound. *};
 
-  let ?S = "{a u :: real | u. u:F}"
+  let ?S = "{a u :: real | u. u:F}";
 
-  have "EX xi. isLub UNIV ?S xi"  
-  proof (rule reals_complete)
+  have "EX xi. isLub UNIV ?S xi";  
+  proof (rule reals_complete);
   
-    txt {* The set $S$ is non-empty, since $a\ap\zero \in S$: *}
+    txt {* The set $S$ is non-empty, since $a\ap\zero \in S$: *};
 
-    from vs have "a 00 : ?S" by force
-    thus "EX X. X : ?S" ..
+    from vs; have "a \<zero> : ?S"; by force;
+    thus "EX X. X : ?S"; ..;
 
-    txt {* $b\ap \zero$ is an upper bound of $S$: *}
+    txt {* $b\ap \zero$ is an upper bound of $S$: *};
 
-    show "EX Y. isUb UNIV ?S Y" 
-    proof 
-      show "isUb UNIV ?S (b 00)"
-      proof (intro isUbI setleI ballI)
-        show "b 00 : UNIV" ..
-      next
+    show "EX Y. isUb UNIV ?S Y"; 
+    proof; 
+      show "isUb UNIV ?S (b \<zero>)";
+      proof (intro isUbI setleI ballI);
+        show "b \<zero> : UNIV"; ..;
+      next;
 
-        txt {* Every element $y\in S$ is less than $b\ap \zero$: *}
+        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 00" 
-        proof
-          fix u assume "u:F" 
-          assume "y = a u"
-          also have "a u <= b 00" by (rule r) (simp!)+
-          finally show ?thesis .
-        qed
-      qed
-    qed
-  qed
+        fix y; assume y: "y : ?S"; 
+        from y; have "EX u:F. y = a u"; by fast;
+        thus "y <= b \<zero>"; 
+        proof;
+          fix u; assume "u:F"; 
+          assume "y = a u";
+          also; have "a u <= b \<zero>"; by (rule r) (simp!)+;
+          finally; show ?thesis; .;
+        qed;
+      qed;
+    qed;
+  qed;
 
-  thus "EX xi. ALL y:F. a y <= xi & xi <= b y" 
-  proof (elim exE)
-    fix xi assume "isLub UNIV ?S xi" 
-    show ?thesis
-    proof (intro exI conjI ballI) 
+  thus "EX xi. ALL y:F. a y <= xi & xi <= b y"; 
+  proof (elim exE);
+    fix xi; assume "isLub UNIV ?S xi"; 
+    show ?thesis;
+    proof (intro exI conjI ballI); 
    
-      txt {* For all $y\in F$ holds $a\ap y \leq \xi$: *}
+      txt {* For all $y\in F$ holds $a\ap y \leq \xi$: *};
      
-      fix y assume y: "y:F"
-      show "a y <= xi"    
-      proof (rule isUbD)  
-        show "isUb UNIV ?S xi" ..
-      qed (force!)
-    next
+      fix y; assume y: "y:F";
+      show "a y <= xi";    
+      proof (rule isUbD);  
+        show "isUb UNIV ?S xi"; ..;
+      qed (force!);
+    next;
 
-      txt {* For all $y\in F$ holds $\xi\leq b\ap y$: *}
+      txt {* For all $y\in F$ holds $\xi\leq b\ap y$: *};
 
-      fix y assume "y:F"
-      show "xi <= b y"  
-      proof (intro isLub_le_isUb isUbI setleI)
-        show "b y : UNIV" ..
-        show "ALL ya : ?S. ya <= b y" 
-        proof
-          fix au assume au: "au : ?S "
-          hence "EX u:F. au = a u" by fast
-          thus "au <= b y"
-          proof
-            fix u assume "u:F" assume "au = a u"  
-            also have "... <= b y" by (rule r)
-            finally show ?thesis .
-          qed
-        qed
-      qed 
-    qed
-  qed
-qed
+      fix y; assume "y:F";
+      show "xi <= b y";  
+      proof (intro isLub_le_isUb isUbI setleI);
+        show "b y : UNIV"; ..;
+        show "ALL ya : ?S. ya <= b y"; 
+        proof;
+          fix au; assume au: "au : ?S ";
+          hence "EX u:F. au = a u"; by fast;
+          thus "au <= b y";
+          proof;
+            fix u; assume "u:F"; assume "au = a u";  
+            also; have "... <= b y"; by (rule r);
+            finally; show ?thesis; .;
+          qed;
+        qed;
+      qed; 
+    qed;
+  qed;
+qed;
 
 text{* \medskip The function $h_0$ is defined as a
 $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$. *}
+is a linear extension of $h$ to $H_0$. *};
 
 lemma h0_lf: 
-  "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H 
+  "[| h0 == (\\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<prod> x0 & y:H 
                 in h y + a * xi);
   H0 == H + lin x0; is_subspace H E; is_linearform H h; x0 ~: H; 
-  x0 : E; x0 ~= 00; is_vectorspace E |]
-  ==> is_linearform H0 h0"
-proof -
+  x0 : E; x0 ~= \<zero>; is_vectorspace E |]
+  ==> is_linearform H0 h0";
+proof -;
   assume h0_def: 
-    "h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H 
+    "h0 == (\\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<prod> x0 & y: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 ~= 00" "x0 : E" "is_vectorspace E"
+      "x0 ~= \<zero>" "x0 : E" "is_vectorspace E";
 
-  have h0: "is_vectorspace H0" 
-  proof (unfold H0_def, rule vs_sum_vs)
-    show "is_subspace (lin x0) E" ..
-  qed 
+  have h0: "is_vectorspace H0"; 
+  proof (unfold H0_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" 
+  show ?thesis;
+  proof;
+    fix x1 x2; assume x1: "x1 : H0" and x2: "x2 : H0"; 
 
     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$. *} 
+    for $x_1, x_2\in H$. *}; 
 
-    have x1x2: "x1 + x2 : H0" 
-      by (rule vs_add_closed, rule h0) 
-    from x1 
-    have ex_x1: "EX y1 a1. x1 = y1 + a1 (*) x0  & y1 : H" 
-      by (unfold H0_def vs_sum_def lin_def) fast
-    from x2 
-    have ex_x2: "EX y2 a2. x2 = y2 + a2 (*) x0 & y2 : H" 
-      by (unfold H0_def vs_sum_def lin_def) fast
-    from x1x2 
-    have ex_x1x2: "EX y a. x1 + x2 = y + a (*) x0 & y : H"
-      by (unfold H0_def vs_sum_def lin_def) fast
+    have x1x2: "x1 + x2 : H0"; 
+      by (rule vs_add_closed, rule h0); 
+    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;
+    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;
+    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;
 
-    from ex_x1 ex_x2 ex_x1x2
-    show "h0 (x1 + x2) = h0 x1 + h0 x2"
-    proof (elim exE conjE)
-      fix y1 y2 y a1 a2 a
-      assume y1: "x1 = y1 + a1 (*) x0"     and y1': "y1 : H"
-         and y2: "x2 = y2 + a2 (*) x0"     and y2': "y2 : H" 
-         and y: "x1 + x2 = y + a (*) x0"   and y':  "y  : H" 
+    from ex_x1 ex_x2 ex_x1x2;
+    show "h0 (x1 + x2) = h0 x1 + h0 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"; 
 
-      have ya: "y1 + y2 = y & a1 + a2 = a" 
-      proof (rule decomp_H0)
-	txt_raw {* \label{decomp-H0-use} *}
-        show "y1 + y2 + (a1 + a2) (*) x0 = y + a (*) x0" 
-          by (simp! add: vs_add_mult_distrib2 [of E])
-        show "y1 + y2 : H" ..
-      qed
+      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"; 
+          by (simp! add: vs_add_mult_distrib2 [of E]);
+        show "y1 + y2 : H"; ..;
+      qed;
 
-      have "h0 (x1 + x2) = h y + a * xi"
-	by (rule h0_definite)
-      also have "... = h (y1 + y2) + (a1 + a2) * xi" 
-        by (simp add: ya)
-      also from vs y1' y2' 
-      have "... = h y1 + h y2 + a1 * xi + a2 * xi" 
+      have "h0 (x1 + x2) = h y + a * xi";
+	by (rule h0_definite);
+      also; have "... = h (y1 + y2) + (a1 + a2) * xi"; 
+        by (simp add: ya);
+      also; from vs y1' y2'; 
+      have "... = h y1 + h y2 + a1 * xi + a2 * xi"; 
 	by (simp add: linearform_add [of H] 
-                      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])
-      finally show ?thesis .
-    qed
+                      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]);
+      finally; show ?thesis; .;
+    qed;
  
     txt{* We further have to show that $h_0$ is multiplicative, 
     i.~e.\ $h_0\ap (c \mult x_1) = c \cdot h_0\ap x_1$
     for $x\in H$ and $c\in \bbbR$. 
-    *} 
+    *}; 
 
-  next  
-    fix c x1 assume x1: "x1 : H0"    
-    have ax1: "c (*) x1 : H0"
-      by (rule vs_mult_closed, rule h0)
-    from x1 have ex_x: "!! x. x: H0 
-                        ==> EX y a. x = y + a (*) x0 & y : H"
-      by (unfold H0_def vs_sum_def lin_def) fast
+  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;
 
-    from x1 have ex_x1: "EX y1 a1. x1 = y1 + a1 (*) x0 & y1 : H"
-      by (unfold H0_def vs_sum_def lin_def) fast
-    with ex_x [of "c (*) x1", OF ax1]
-    show "h0 (c (*) x1) = c * (h0 x1)"  
-    proof (elim exE conjE)
-      fix y1 y a1 a 
-      assume y1: "x1 = y1 + a1 (*) x0"       and y1': "y1 : H"
-        and y: "c (*) x1 = y  + a  (*) x0"   and y':  "y  : 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;
+    with ex_x [of "c \<prod> x1", OF ax1];
+    show "h0 (c \<prod> x1) = c * (h0 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"; 
 
-      have ya: "c (*) y1 = y & c * a1 = a" 
-      proof (rule decomp_H0) 
-	show "c (*) y1 + (c * a1) (*) x0 = y + a (*) x0" 
-          by (simp! add: add: vs_add_mult_distrib1)
-        show "c (*) y1 : H" ..
-      qed
+      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"; ..;
+      qed;
 
-      have "h0 (c (*) x1) = h y + a * xi" 
-	by (rule h0_definite)
-      also have "... = h (c (*) 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])
-      finally show ?thesis .
-    qed
-  qed
-qed
+      have "h0 (c \<prod> x1) = h y + a * xi"; 
+	by (rule h0_definite);
+      also; have "... = h (c \<prod> 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]);
+      finally; show ?thesis; .;
+    qed;
+  qed;
+qed;
 
 text{* \medskip The linear extension $h_0$ of $h$
-is bounded by the seminorm $p$. *}
+is bounded by the seminorm $p$. *};
 
 lemma h0_norm_pres:
-  "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H 
+  "[| h0 == (\\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<prod> x0 & y:H 
                 in h y + a * xi);
-  H0 == H + lin x0; x0 ~: H; x0 : E; x0 ~= 00; is_vectorspace E; 
+  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" 
-proof 
+   ==> ALL x:H0. h0 x <= p x"; 
+proof; 
   assume h0_def: 
-    "h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H 
+    "h0 == (\\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<prod> x0 & y:H 
                in (h y) + a * xi)"
     and H0_def: "H0 == H + lin x0" 
-    and vs: "x0 ~: H" "x0 : E" "x0 ~= 00" "is_vectorspace E" 
+    and vs: "x0 ~: H" "x0 : E" "x0 ~= \<zero>" "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: "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"; 
   have ex_x: 
-    "!! x. x : H0 ==> EX y a. x = y + a (*) x0 & y : H"
-    by (unfold H0_def vs_sum_def lin_def) fast
-  have "EX y a. x = y + a (*) x0 & y : H"
-    by (rule ex_x)
-  thus "h0 x <= p x"
-  proof (elim exE conjE)
-    fix y a assume x: "x = y + a (*) x0" and y: "y : H"
-    have "h0 x = h y + a * xi"
-      by (rule h0_definite)
+    "!! 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";
+    by (rule ex_x);
+  thus "h0 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);
 
     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}*}
+    by case analysis on $a$. \label{linorder_linear_split}*};
 
-    also have "... <= p (y + a (*) x0)"
-    proof (rule linorder_linear_split) 
+    also; have "... <= p (y + a \<prod> x0)";
+    proof (rule linorder_linear_split); 
 
-      assume z: "a = #0"
-      with vs y a show ?thesis by simp
+      assume z: "a = #0"; 
+      with vs y a; show ?thesis; by simp;
 
     txt {* In the case $a < 0$, we use $a_1$ with $\idt{ya}$ 
-    taken as $y/a$: *}
+    taken as $y/a$: *};
 
-    next
-      assume lz: "a < #0" hence nz: "a ~= #0" by simp
-      from a1 
-      have "- p (rinv a (*) y + x0) - h (rinv a (*) y) <= xi"
-        by (rule bspec) (simp!)
+    next;
+      assume lz: "a < #0"; hence nz: "a ~= #0"; by simp;
+      from a1; 
+      have "- p (rinv a \<prod> y + x0) - h (rinv a \<prod> y) <= xi";
+        by (rule bspec) (simp!);
 
       txt {* The thesis for this case now follows by a short  
-      calculation. *}      
+      calculation. *};      
       hence "a * xi 
-            <= a * (- p (rinv a (*) y + x0) - h (rinv a (*) y))"
-        by (rule real_mult_less_le_anti [OF lz])
-      also have "... = - a * (p (rinv a (*) y + x0)) 
-                        - a * (h (rinv a (*) y))"
-        by (rule real_mult_diff_distrib)
-      also from lz vs y have "- a * (p (rinv a (*) y + x0)) 
-                               = p (a (*) (rinv a (*) y + x0))"
-        by (simp add: seminorm_abs_homogenous abs_minus_eqI2)
-      also from nz vs y have "... = p (y + a (*) x0)"
-        by (simp add: vs_add_mult_distrib1)
-      also from nz vs y have "a * (h (rinv a (*) y)) =  h y"
-        by (simp add: linearform_mult [RS sym])
-      finally have "a * xi <= p (y + a (*) x0) - h y" .
+            <= a * (- p (rinv a \<prod> y + x0) - h (rinv a \<prod> 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))";
+        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))";
+        by (simp add: seminorm_abs_homogenous abs_minus_eqI2);
+      also; from nz vs y; have "... = p (y + a \<prod> x0)";
+        by (simp add: vs_add_mult_distrib1);
+      also; from nz vs y; have "a * (h (rinv a \<prod> y)) =  h y";
+        by (simp add: linearform_mult [RS sym]);
+      finally; have "a * xi <= p (y + a \<prod> x0) - h y"; .;
 
-      hence "h y + a * xi <= h y + p (y + a (*) x0) - h y"
-        by (simp add: real_add_left_cancel_le)
-      thus ?thesis by simp
+      hence "h y + a * xi <= h y + p (y + a \<prod> x0) - h y";
+        by (simp add: real_add_left_cancel_le);
+      thus ?thesis; by simp;
 
       txt {* In the case $a > 0$, we use $a_2$ with $\idt{ya}$ 
-      taken as $y/a$: *}
+      taken as $y/a$: *};
 
-    next 
-      assume gz: "#0 < a" hence nz: "a ~= #0" by simp
-      from a2
-      have "xi <= p (rinv a (*) y + x0) - h (rinv a (*) y)"
-        by (rule bspec) (simp!)
+    next; 
+      assume gz: "#0 < a"; hence nz: "a ~= #0"; by simp;
+      from a2;
+      have "xi <= p (rinv a \<prod> y + x0) - h (rinv a \<prod> y)";
+        by (rule bspec) (simp!);
 
       txt {* The thesis for this case follows by a short
-      calculation: *}
+      calculation: *};
 
-      with gz have "a * xi 
-            <= a * (p (rinv a (*) y + x0) - h (rinv a (*) y))"
-        by (rule real_mult_less_le_mono)
-      also have "... = a * p (rinv a (*) y + x0) 
-                        - a * h (rinv a (*) y)"
-        by (rule real_mult_diff_distrib2) 
-      also from gz vs y 
-      have "a * p (rinv a (*) y + x0) 
-           = p (a (*) (rinv a (*) y + x0))"
-        by (simp add: seminorm_abs_homogenous abs_eqI2)
-      also from nz vs y 
-      have "... = p (y + a (*) x0)"
-        by (simp add: vs_add_mult_distrib1)
-      also from nz vs y have "a * h (rinv a (*) y) = h y"
-        by (simp add: linearform_mult [RS sym]) 
-      finally have "a * xi <= p (y + a (*) x0) - h y" .
+      with gz; have "a * xi 
+            <= a * (p (rinv a \<prod> y + x0) - h (rinv a \<prod> y))";
+        by (rule real_mult_less_le_mono);
+      also; have "... = a * p (rinv a \<prod> y + x0) 
+                        - a * h (rinv a \<prod> 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))";
+        by (simp add: seminorm_abs_homogenous abs_eqI2);
+      also; from nz vs y; 
+      have "... = p (y + a \<prod> x0)";
+        by (simp add: vs_add_mult_distrib1);
+      also; from nz vs y; have "a * h (rinv a \<prod> y) = h y";
+        by (simp add: linearform_mult [RS sym]); 
+      finally; have "a * xi <= p (y + a \<prod> x0) - h y"; .;
  
-      hence "h y + a * xi <= h y + (p (y + a (*) x0) - h y)"
-        by (simp add: real_add_left_cancel_le)
-      thus ?thesis by simp
-    qed
-    also from x have "... = p x" by simp
-    finally show ?thesis .
-  qed
-qed blast+ 
+      hence "h y + a * xi <= h y + (p (y + a \<prod> x0) - h y)";
+        by (simp add: real_add_left_cancel_le);
+      thus ?thesis; by simp;
+    qed;
+    also; from x; have "... = p x"; by simp;
+    finally; show ?thesis; .;
+  qed;
+qed blast+; 
 
-end
\ No newline at end of file
+end;
\ No newline at end of file
diff -r 2ceb11a2e190 -r f9a6670427fb src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Thu Jul 06 09:46:56 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Thu Jul 06 10:10:10 2000 +0200
@@ -3,9 +3,10 @@
     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:;
+
 
 
 text{* This section contains some lemmas that will be used in the
@@ -17,7 +18,7 @@
 $\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:
@@ -62,7 +63,7 @@
 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; 
@@ -70,78 +71,78 @@
    ==> 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)"
-proof -
+       & (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"
+     and u: "graph H h = Union c" "x: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)
+  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 
                   & 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' 
+                  & (ALL x:H'. h' x <= p x)";
+      by (rule norm_pres_extension_D);
+    thus ?thesis;
+    proof (elim exE conjE); 
+      fix H' h'; 
       assume "graph H' h' = g" "is_linearform H' h'" 
         "is_subspace H' E" "is_subspace F H'" 
-        "graph F f <= 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 <= 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;
 
 
 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 
       & 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 -
+      & 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"  
+     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"
+       & (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 <= 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;
 
 (***
 lemma some_H'h': 
@@ -185,81 +186,81 @@
 
 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 
       & 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 -
+      & 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 H h = Union c" "x:H" "y: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'
        & 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)
+       & (ALL x:H'. h' x <= p x)";
+    by (rule some_H'h't);
 
   txt {* $y$ is in the domain $H''$ of some function $h''$,
-  such that $h$ extends $h''$. *} 
+  such that $h$ extends $h''$. *}; 
 
   have e2: "EX H'' h''. graph H'' h'' : c & (y, h y) : 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)
+       & (ALL x:H''. h'' x <= p x)";
+    by (rule some_H'h't);
 
-  from e1 e2 show ?thesis 
-  proof (elim exE conjE)
-    fix H' h' assume "(y, h y): graph H' h'" "graph H' h' : c"
+  from e1 e2; show ?thesis; 
+  proof (elim exE conjE);
+    fix H' h'; assume "(y, h y): 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"
+      "graph F f <= graph H' h'" "ALL x:H'. h' x <= p x";
 
-    fix H'' h'' assume "(x, h x): graph H'' h''" "graph H'' h'' : c"
+    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"
+      "graph F f <= graph H'' h''" "ALL x:H''. h'' x <= p x";
 
    txt {* Since both $h'$ and $h''$ are elements of the chain,  
    $h''$ is an extension of $h'$ or vice versa. Thus both 
-   $x$ and $y$ are contained in the greater one. \label{cases1}*}
+   $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
+      (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;
 
 (***
 lemma some_H'h'2: 
@@ -336,303 +337,303 @@
 ***)
 
 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 - 
+  (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)
+    "(x, y) : Union c" "(x, z) : 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) : G1" "G1 : c" "(x, z) : G2" "G2 : c" "c <= 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 : 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";
 
       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 <= 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;
 
 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 - 
+  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"
+         "graph H h = Union c";
  
-  show "is_linearform H h"
-  proof
-    fix x y assume "x : H" "y : H" 
+  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 
             & 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)
+            & (ALL x:H'. h' x <= 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'" 
+    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"
+        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 
             & 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')
+            & (ALL x:H'. h' x <= 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 (*) x) = a * h x"
-    proof (elim exE conjE)
-      fix H' h' assume "x:H'"
+    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 (*) x) = a * h' x" 
-        by (rule linearform_mult)
-      also have "h' x = h x" ..
-      also have "a (*) x : H'" ..
-      with b have "h' (a (*) x) = h (a (*) x)" ..
-      finally show ?thesis .
-    qed
-  qed
-qed
+        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;
 
 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 -
+  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!)
+         "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!);
 
     hence "EX 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)
+             & (ALL x:G. g x <= p x)";
+      by (simp! add: norm_pres_extension_D);
 
-    thus ?thesis 
-    proof (elim exE conjE) 
-      fix G g assume "graph F f <= 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 <= 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;
 
 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;
   graph H h = Union c; is_subspace F E; is_vectorspace E |] 
-  ==> is_subspace F H"
-proof - 
+  ==> 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"
+    "graph H h = Union c" "is_subspace F E" "is_vectorspace E";
 
-  show ?thesis 
-  proof
-    show "00 : 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 (*) x : F"
-    proof (intro ballI allI)
-      fix x a assume "x:F"
-      show "a (*) x : F" by (simp!)
-    qed
-  qed
-qed
+  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;
 
 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; 
   graph H h = Union c; is_subspace F E; is_vectorspace E |] 
-  ==> is_subspace H E"
-proof - 
+  ==> 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
+    "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 "00 : F" ..
-    also have "is_subspace F H" by (rule sup_supF) 
-    hence "F <= H" ..
-    finally show "00 : H" .
+    have "\<zero> : F"; ..;
+    also; have "is_subspace F H"; by (rule sup_supF); 
+    hence "F <= H"; ..;
+    finally; show "\<zero> : H"; .;
 
-    txt{* $H$ is a subset of $E$: *}
+    txt{* $H$ is a subset of $E$: *};
 
-    show "H <= E" 
-    proof
-      fix x assume "x:H"
+    show "H <= E"; 
+    proof;
+      fix x; assume "x:H";
       have "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)" 
-	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
+              & (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;
 
-    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"
+    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 
               & 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' 
+              & (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      
+          "graph H' h' <= graph H h";
+        have "x + y : H'"; ..;
+	also; have "H' <= 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 (*) x : H" 
-    proof (intro ballI allI) 
-      fix x a assume "x:H" 
+    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
               & 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 (*) x : H" 
-      proof (elim exE conjE)
-	fix H' h' 
-        assume "x:H'" "is_subspace H' E" "graph H' h' <= graph H h"
-        have "a (*) x : H'" ..
-        also have "H' <= H" ..
-	finally show ?thesis .
-      qed
-    qed
-  qed
-qed
+              & (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;
 
 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
+  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"
+         "graph H h = Union c";
+  fix x; assume "x:H";
   have "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)" 
-    by (rule some_H'h')
-  thus "h x <= p x" 
-  proof (elim exE conjE)
-    fix H' 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
+      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;
 
 
 text{* \medskip The following lemma is a property of linear forms on 
@@ -643,47 +644,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 -
+  (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: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;  
 
 
-end
\ No newline at end of file
+end;
\ No newline at end of file