# HG changeset patch
# User wenzelm
# Date 941221114 -7200
# Node ID 1b99ee57d1311d264ae74b35b6b217851f8e6eda
# Parent  67bfcd3a433c86f1278433d7ef09c40ef7c7ad56
final update by Gertrud Bauer;

diff -r 67bfcd3a433c -r 1b99ee57d131 src/HOL/Real/HahnBanach/Aux.thy
--- a/src/HOL/Real/HahnBanach/Aux.thy	Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Aux.thy	Fri Oct 29 20:18:34 1999 +0200
@@ -15,7 +15,7 @@
 lemmas chainE2 = chainD2 [elimify];
 
 text_raw {* \medskip *};
-text{* Lemmas about sets: *};
+text{* Lemmas about sets. *};
 
 lemma Int_singletonD: "[| A Int B = {v}; x:A; x:B |] ==> x = v";
   by (fast elim: equalityE);
@@ -24,7 +24,7 @@
  by (force simp add: psubset_eq);
 
 text_raw {* \medskip *};
-text{* Some lemmas about orders: *};
+text{* Some lemmas about orders. *};
 
 lemma lt_imp_not_eq: "x < (y::'a::order) ==> x ~= y"; 
   by (rule order_less_le[RS iffD1, RS conjunct2]);
diff -r 67bfcd3a433c -r 1b99ee57d131 src/HOL/Real/HahnBanach/Bounds.thy
--- a/src/HOL/Real/HahnBanach/Bounds.thy	Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Bounds.thy	Fri Oct 29 20:18:34 1999 +0200
@@ -71,10 +71,12 @@
 
 text_raw {* \end{comment} *};
 
-text {* A supremum of an ordered set $B$ w.~r.~t.~$A$ 
-is defined as a least upperbound of $B$, which lies in $A$.
-The definition of the supremum is based on the
-existing definition (see HOL/Real/Lubs.thy).*};
+text {*
+ A supremum\footnote{The definition of the supremum is based on one in
+ \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Lubs.html}}  of
+ an ordered set $B$ w.~r.~t.~$A$ is defined as a least upper bound of
+ $B$, which lies in $A$.
+*};
    
 text{* If a supremum exists, then $\idt{Sup}\ap A\ap B$
 is equal to the supremum. *};
@@ -114,13 +116,13 @@
 text_raw {* \end{comment} *};
 ;
 
-text{* The supremum of $B$ is less than every upper bound
+text{* The supremum of $B$ is less than any upper bound
 of $B$.*};
 
 lemma sup_le_ub: "isUb A B y ==> is_Sup A B s ==> s <= y";
   by (unfold is_Sup_def, rule isLub_le_isUb);
 
-text {* The supremum $B$ is an upperbound for $B$. *};
+text {* The supremum $B$ is an upper bound for $B$. *};
 
 lemma sup_ub: "y:B ==> is_Sup A B s ==> y <= s";
   by (unfold is_Sup_def, rule isLubD2);
diff -r 67bfcd3a433c -r 1b99ee57d131 src/HOL/Real/HahnBanach/FunctionNorm.thy
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Fri Oct 29 20:18:34 1999 +0200
@@ -7,110 +7,113 @@
 
 theory FunctionNorm = NormedSpace + FunctionOrder:;
 
-subsection {* Continous linearforms*};
+subsection {* Continuous linear forms*};
 
-text{* A linearform $f$ on a normed vector space $(V, \norm{\cdot})$
-is \emph{continous}, iff it is bounded, i.~e.
-\[\exists\ap c\in R.\ap \forall\ap x\in V.\ap 
-|f\ap x| \leq c \cdot \norm x\]
-In our application no other functions than linearforms are considered,
-so we can define continous linearforms as follows:
+text{* A linear form $f$ on a normed vector space $(V, \norm{\cdot})$
+is \emph{continuous}, iff it is bounded, i.~e.
+\[\Ex {c\in R}{\All {x\in V} {|f\ap x| \leq c \cdot \norm x}}\]
+In our application no other functions than linear forms are considered,
+so we can define continuous linear forms as bounded linear forms:
 *};
 
 constdefs
-  is_continous ::
+  is_continuous ::
   "['a::{minus, plus} set, 'a => real, 'a => real] => bool" 
-  "is_continous V norm f == 
+  "is_continuous V norm f == 
     is_linearform V f & (EX c. ALL x:V. rabs (f x) <= c * norm x)";
 
-lemma continousI [intro]: 
+lemma continuousI [intro]: 
   "[| is_linearform V f; !! x. x:V ==> rabs (f x) <= c * norm x |] 
-  ==> is_continous V norm f";
-proof (unfold is_continous_def, intro exI conjI ballI);
+  ==> is_continuous V norm f";
+proof (unfold is_continuous_def, intro exI conjI ballI);
   assume r: "!! x. x:V ==> rabs (f x) <= c * norm x"; 
   fix x; assume "x:V"; show "rabs (f x) <= c * norm x"; by (rule r);
 qed;
   
-lemma continous_linearform [intro!!]: 
-  "is_continous V norm f ==> is_linearform V f";
-  by (unfold is_continous_def) force;
+lemma continuous_linearform [intro!!]: 
+  "is_continuous V norm f ==> is_linearform V f";
+  by (unfold is_continuous_def) force;
 
-lemma continous_bounded [intro!!]:
-  "is_continous V norm f 
+lemma continuous_bounded [intro!!]:
+  "is_continuous V norm f 
   ==> EX c. ALL x:V. rabs (f x) <= c * norm x";
-  by (unfold is_continous_def) force;
+  by (unfold is_continuous_def) force;
 
-subsection{* The norm of a linearform *};
+subsection{* The norm of a linear form *};
 
 
 text{* The least real number $c$ for which holds
-\[\forall\ap x\in V.\ap |f\ap x| \leq c \cdot \norm x\]
+\[\All {x\in V}{|f\ap x| \leq c \cdot \norm x}\]
 is called the \emph{norm} of $f$.
 
-For the non-trivial vector space $V$ the norm can be defined as 
+For non-trivial vector spaces $V \neq \{\zero\}$ the norm can be defined as 
 \[\fnorm {f} =\sup_{x\neq\zero}\frac{|f\ap x|}{\norm x} \] 
 
-For the case that the vector space $V$ contains only the $\zero$
-vector, the set $B$ this supremum is taken from would be empty, and
-any real number is a supremum of $B$. So it must be guarateed that
-there is an element in $B$. This element must be ${} \ge 0$ so that
+For the case $V = \{\zero\}$ the supremum would be taken from an
+empty set. Since $\bbbR$ is unbounded, there would be no supremum.  To
+avoid this situation it must be guaranteed that there is an element in
+this set. This element must be ${} \ge 0$ so that
 $\idt{function{\dsh}norm}$ has the norm properties. Furthermore it
 does not have to change the norm in all other cases, so it must be
-$0$, as all other elements of $B$ are ${} \ge 0$.
+$0$, as all other elements of are ${} \ge 0$.
 
-Thus $B$ is defined as follows.
+Thus we define the set $B$ the supremum is taken from as
+\[
+\{ 0 \} \Un \left\{ \frac{|f\ap x|}{\norm x} \dt x\neq \zero \And x\in F\right\}
+ \]
 *};
 
 constdefs
   B :: "[ 'a set, 'a => real, 'a => real ] => real set"
   "B V norm f == 
-  {z. z = 0r | (EX x:V. x ~= <0> & z = rabs (f x) * rinv (norm x))}";
-
-text{* $\idt{function{\dsh}norm}$ is equal to the supremum of $B$, 
-if there exists a supremum. *};
+  {0r} \Un {rabs (f x) * rinv (norm x) | x. x ~= <0> & x:V}";
 
-constdefs 
-  function_norm :: " ['a set, 'a => real, 'a => real] => real"
-  "function_norm V norm f == Sup UNIV (B V norm f)";
-
-text{* $\idt{is{\dsh}function{\dsh}norm}$ also guarantees that there 
-is a funciton norm .*};
+text{* $n$ is the function norm of $f$, iff 
+$n$ is the supremum of $B$. 
+*};
 
 constdefs 
   is_function_norm :: 
   " ['a set, 'a => real, 'a => real] => real => bool"
   "is_function_norm V norm f fn == is_Sup UNIV (B V norm f) fn";
 
+text{* $\idt{function{\dsh}norm}$ is equal to the supremum of $B$, 
+if the supremum exists. Otherwise it is undefined. *};
+
+constdefs 
+  function_norm :: " ['a set, 'a => real, 'a => real] => real"
+  "function_norm V norm f == Sup UNIV (B V norm f)";
+
 lemma B_not_empty: "0r : B V norm f";
   by (unfold B_def, force);
 
-text {* The following lemma states every continous linearform on a 
-normed space $(V, \norm{\cdot})$ has a function norm. *};
+text {* The following lemma states that every continuous linear form
+on a normed space $(V, \norm{\cdot})$ has a function norm. *};
 
 lemma ex_fnorm [intro!!]: 
-  "[| is_normed_vectorspace V norm; is_continous V norm f|]
+  "[| is_normed_vectorspace V norm; is_continuous V norm f|]
      ==> is_function_norm V norm f (function_norm V norm f)"; 
 proof (unfold function_norm_def is_function_norm_def 
-  is_continous_def Sup_def, elim conjE, rule selectI2EX);
+  is_continuous_def Sup_def, elim conjE, rule selectI2EX);
   assume "is_normed_vectorspace V norm";
   assume "is_linearform V f" 
   and e: "EX c. ALL x:V. rabs (f x) <= c * norm x";
 
   txt {* The existence of the supremum is shown using the 
   completeness of the reals. Completeness means, that
-  for every non-empty and bounded set of reals there exists a 
+  every non-empty bounded set of reals has a 
   supremum. *};
   show  "EX a. is_Sup UNIV (B V norm f) a"; 
   proof (unfold is_Sup_def, rule reals_complete);
 
-    txt {* First we have to show that $B$ is non-empty. *}; 
+    txt {* First we have to show that $B$ is non-empty: *}; 
 
     show "EX X. X : B V norm f"; 
     proof (intro exI);
       show "0r : (B V norm f)"; by (unfold B_def, force);
     qed;
 
-    txt {* Then we have to show that $B$ is bounded. *};
+    txt {* Then we have to show that $B$ is bounded: *};
 
     from e; show "EX Y. isUb UNIV (B V norm f) Y";
     proof;
@@ -122,19 +125,18 @@
 
       show "?thesis";
       proof (intro exI isUbI setleI ballI, unfold B_def, 
-	elim CollectE disjE bexE conjE);
+	elim UnE CollectE exE conjE singletonE);
 
         txt{* To proof the thesis, we have to show that there is 
-        some constant b, which is greater than every $y$ in $B$. 
+        some constant $b$, such that $y \leq b$ for all $y\in B$. 
         Due to the definition of $B$ there are two cases for
-        $y\in B$. If $y = 0$ then $y$ is less than 
-        $\idt{max}\ap c\ap 0$: *};
+        $y\in B$. If $y = 0$ then $y \leq idt{max}\ap c\ap 0$: *};
 
 	fix y; assume "y = 0r";
         show "y <= b"; by (simp! add: le_max2);
 
         txt{* The second case is 
-        $y = \frac{|f\ap x|}{\norm x}$ for some 
+        $y = {|f\ap x|}/{\norm x}$ for some 
         $x\in V$ with $x \neq \zero$. *};
 
       next;
@@ -186,13 +188,13 @@
   qed;
 qed;
 
-text {* The norm of a continous function is always $\geq 0$. *};
+text {* The norm of a continuous function is always $\geq 0$. *};
 
 lemma fnorm_ge_zero [intro!!]: 
-  "[| is_continous V norm f; is_normed_vectorspace V norm|]
+  "[| is_continuous V norm f; is_normed_vectorspace V norm|]
    ==> 0r <= function_norm V norm f";
 proof -;
-  assume c: "is_continous V norm f" 
+  assume c: "is_continuous V norm f" 
      and n: "is_normed_vectorspace V norm";
 
   txt {* The function norm is defined as the supremum of $B$. 
@@ -202,9 +204,9 @@
   show ?thesis; 
   proof (unfold function_norm_def, rule sup_ub1);
     show "ALL x:(B V norm f). 0r <= x"; 
-    proof (intro ballI, unfold B_def, 
-           elim CollectE bexE conjE disjE);
-      fix x r; 
+    proof (intro ballI, unfold B_def,
+           elim UnE singletonE CollectE exE conjE); 
+      fix x r;
       assume "x : V" "x ~= <0>" 
         and r: "r = rabs (f x) * rinv (norm x)";
 
@@ -218,33 +220,33 @@
           qed;
         qed; ***)
       with ge; show "0r <= r";
-       by (simp only: r,rule real_le_mult_order);
+       by (simp only: r, rule real_le_mult_order);
     qed (simp!);
 
-    txt {* Since $f$ is continous the function norm exists. *};
+    txt {* Since $f$ is continuous the function norm exists: *};
 
     have "is_function_norm V norm f (function_norm V norm f)"; ..;
     thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"; 
-      by (unfold is_function_norm_def, unfold function_norm_def);
+      by (unfold is_function_norm_def function_norm_def);
 
-    txt {* $B$ is non-empty by construction. *};
+    txt {* $B$ is non-empty by construction: *};
 
     show "0r : B V norm f"; by (rule B_not_empty);
   qed;
 qed;
   
-text{* The basic property of function norms is: 
+text{* \medskip The fundamental property of function norms is: 
 \begin{matharray}{l}
 | f\ap x | \leq {\fnorm {f}} \cdot {\norm x}  
 \end{matharray}
 *};
 
 lemma norm_fx_le_norm_f_norm_x: 
-  "[| is_normed_vectorspace V norm; x:V; is_continous V norm f |] 
-    ==> rabs (f x) <= (function_norm V norm f) * norm x"; 
+  "[| is_normed_vectorspace V norm; x:V; is_continuous V norm f |] 
+    ==> rabs (f x) <= function_norm V norm f * norm x"; 
 proof -; 
   assume "is_normed_vectorspace V norm" "x:V" 
-  and c: "is_continous V norm f";
+  and c: "is_continuous V norm f";
   have v: "is_vectorspace V"; ..;
   assume "x:V";
 
@@ -259,7 +261,7 @@
 
     assume "x = <0>";
     have "rabs (f x) = rabs (f <0>)"; by (simp!);
-    also; from v continous_linearform; have "f <0> = 0r"; ..;
+    also; from v continuous_linearform; have "f <0> = 0r"; ..;
     also; note rabs_zero;
     also; have "0r <= function_norm V norm f * norm x";
     proof (rule real_le_mult_order);
@@ -286,11 +288,11 @@
       show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))";
          by (simp! add: is_function_norm_def function_norm_def);
       show "rabs (f x) * rinv (norm x) : B V norm f"; 
-        by (unfold B_def, intro CollectI disjI2 bexI [of _ x]
+        by (unfold B_def, intro UnI2 CollectI exI [of _ x]
             conjI, simp);
     qed;
 
-    txt {* The thesis follows by a short calculation: *};
+    txt {* The thesis now follows by a short calculation: *};
 
     have "rabs (f x) = rabs (f x) * 1r"; by (simp!);
     also; from nz; have "1r = rinv (norm x) * norm x"; 
@@ -305,21 +307,20 @@
   qed;
 qed;
 
-text{* The function norm is the least positive real number for 
-which the inequation
+text{* \medskip The function norm is the least positive real number for 
+which the following inequation holds:
 \begin{matharray}{l}
 | f\ap x | \leq c \cdot {\norm x}  
 \end{matharray} 
-holds.
 *};
 
 lemma fnorm_le_ub: 
-  "[| is_normed_vectorspace V norm; is_continous V norm f;
+  "[| is_normed_vectorspace V norm; is_continuous V norm f;
      ALL x:V. rabs (f x) <= c * norm x; 0r <= c |]
   ==> function_norm V norm f <= c";
 proof (unfold function_norm_def);
   assume "is_normed_vectorspace V norm"; 
-  assume c: "is_continous V norm f";
+  assume c: "is_continuous V norm f";
   assume fb: "ALL x:V. rabs (f x) <= c * norm x"
          and "0r <= c";
 
@@ -342,7 +343,7 @@
     proof (intro isUbI setleI ballI);
       fix y; assume "y: B V norm f";
       thus le: "y <= c";
-      proof (unfold B_def, elim CollectE disjE bexE conjE);
+      proof (unfold B_def, elim UnE CollectE exE conjE singletonE);
 
        txt {* The first case for $y\in B$ is $y=0$. *};
 
@@ -350,7 +351,7 @@
         show "y <= c"; by (force!);
 
         txt{* The second case is 
-        $y = \frac{|f\ap x|}{\norm x}$ for some 
+        $y = {|f\ap x|}/{\norm x}$ for some 
         $x\in V$ with $x \neq \zero$. *};  
 
       next;
diff -r 67bfcd3a433c -r 1b99ee57d131 src/HOL/Real/HahnBanach/FunctionOrder.thy
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Fri Oct 29 20:18:34 1999 +0200
@@ -3,29 +3,26 @@
     Author:     Gertrud Bauer, TU Munich
 *)
 
-header {* An Order on functions *};
+header {* An order on functions *};
 
 theory FunctionOrder = Subspace + Linearform:;
 
-
 subsection {* The graph of a function *};
 
-text{* We define the \emph{graph} of a (real) function $f$ with the 
+text{* We define the \emph{graph} of a (real) function $f$ with
 domain $F$ as the set 
 \[
 \{(x, f\ap x). \ap x:F\}
 \]
-So we are modelling partial functions by specifying the domain and 
-the mapping function. We use the notion ``function'' also for the graph
-of a function. 
+So we are modeling partial functions by specifying the domain and 
+the mapping function. We use the term ``function'' also for its graph.
 *};
 
-types 'a graph = "('a::{minus, plus} * real) set";
+types 'a graph = "('a * real) set";
 
 constdefs
   graph :: "['a set, 'a => real] => 'a graph "
-  "graph F f == {p. EX x. p = (x, f x) & x:F}"; (* 
-   == {(x, f x). x:F} *)
+  "graph F f == {(x, f x) | x. x:F}"; 
 
 lemma graphI [intro!!]: "x:F ==> (x, f x) : graph F f";
   by (unfold graph_def, intro CollectI exI) force;
@@ -41,7 +38,7 @@
 
 subsection {* Functions ordered by domain extension *};
 
-text{* The function $h'$ is an extension of $h$, iff the graph of 
+text{* A function $h'$ is an extension of $h$, iff the graph of 
 $h$ is a subset of the graph of $h'$.*};
 
 lemma graph_extI: 
@@ -83,7 +80,7 @@
 lemma graph_domain_funct: 
   "(!!x y z. (x, y):g ==> (x, z):g ==> z = y) 
   ==> graph (domain g) (funct g) = g";
-proof (unfold domain_def, unfold funct_def, unfold graph_def, auto);
+proof (unfold domain_def funct_def graph_def, auto);
   fix a b; assume "(a, b) : g";
   show "(a, SOME y. (a, y) : g) : g"; by (rule selectI2);
   show "EX y. (a, y) : g"; ..;
@@ -96,9 +93,9 @@
 
 
 
-subsection {* Norm preserving extensions of a function *};
+subsection {* Norm-preserving extensions of a function *};
 
-text {* Given a function $f$ on the space $F$ and a quasinorm $p$ on 
+text {* Given a linear form $f$ on the space $F$ and a seminorm $p$ on 
 $E$. The set of all linear extensions of $f$, to superspaces $H$ of 
 $F$, which are bounded by $p$, is defined as follows. *};
 
diff -r 67bfcd3a433c -r 1b99ee57d131 src/HOL/Real/HahnBanach/HahnBanach.thy
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Fri Oct 29 20:18:34 1999 +0200
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Real/HahnBanach/HahnBanach.thy
     ID:         $Id$
-    Author:     Gertrud Baueer, TU Munich
+    Author:     Gertrud Bauer, TU Munich
 *)
 
 header {* The Hahn-Banach Theorem *};
@@ -15,18 +15,19 @@
 
 subsection {* The case of general linear spaces *};
 
-text  {* Every linearform $f$ on a subspace $F$ of $E$, which is 
- bounded by some  quasinorm $q$ on $E$, can be extended 
- to a function on $E$ in a norm preseving way. *};
+text  {* Let $f$ be a linear form $f$ defined on a subspace $F$ 
+ of a norm vector space $E$. If $f$ is  
+ bounded by some seminorm $q$ on $E$, it can be extended 
+ to a function on $E$ in a norm-preserving way. *};
 
 theorem HahnBanach: 
-  "[| is_vectorspace E; is_subspace F E; is_quasinorm E p; 
+  "[| 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_quasinorm E 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{* We define $M$ to be the set of all linear extensions 
@@ -42,19 +43,18 @@
     thus "is_subspace F F"; ..;
   qed (blast!)+;
 
-  subsubsect {* Existence of a limit function of the norm preserving
+  subsubsect {* Existence of a limit function the norm-preserving
   extensions *}; 
 
-  txt {* For every non-empty chain of norm preserving functions
-  the union of all functions in the chain is again a norm preserving
-  function. (The union is an upper bound for all elements. 
+  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$.) *};
 
-  have "!! c. [| c : chain M; EX x. x:c |] ==> Union c : M";  
-  proof -;
+  {{;
     fix c; assume "c:chain M" "EX x. x:c";
-    show "Union c : M";
+    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
@@ -67,29 +67,25 @@
         let ?H = "domain (Union c)";
         let ?h = "funct (Union c)";
 
-        show a [simp]: "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";
           show "z = y"; by (rule sup_definite);
         qed;
             
-        show "is_linearform ?H ?h"; 
+        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;
-  qed;
+  }};
  
   txt {* According to Zorn's Lemma there is
   a maximal norm-preserving extension $g\in M$. *};
@@ -120,19 +116,18 @@
       have h: "is_vectorspace H"; ..;
       have f: "is_vectorspace F"; ..;
 
-subsubsect {* The domain of the limit function. *};
+subsubsect {* The domain of the limit function *};
 
 have eq: "H = E"; 
 proof (rule classical);
 
-txt {* Assume the domain of the supremum is not $E$. *};
+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 
-  the difference of $E$ and $H$. *};
+  txt{* then there exists an element $x_0$ in $E \ H$: *};
 
   hence "EX x0:E. x0~:H"; 
     by (rule set_less_imp_diff_not_empty);
@@ -153,16 +148,16 @@
     qed blast;
 
     txt {* Define $H_0$ as the (direct) sum of H and the 
-    linear closure of $x_0$.*};
+    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)
-                     & (ALL y:H. xi <= p (y + x0) - h y)";
+    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_linear);
+         by (simp! add: linearform_diff);
       also; from h_bound; have "... <= p (v - u)";
         by (simp!);
       also; have "v - u = x0 + - x0 + v + - u";
@@ -172,7 +167,7 @@
       also; have "... = (v + x0) - (u + x0)";
         by (simp! add: diff_eq1);
       also; have "p ... <= p (v + x0) + p (u + x0)";
-         by (rule quasinorm_diff_triangle_ineq) (simp!)+;
+         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";
@@ -182,13 +177,14 @@
                & graph H0 h0 : M"; 
     proof (elim exE, intro exI conjI);
       fix xi; 
-      assume a: "(ALL y:H. - p (y + x0) - h y <= xi) 
-               & (ALL y:H. xi <= p (y + x0) - h y)";
+      assume a: "ALL y:H. - p (y + x0) - h y <= xi 
+                        & xi <= p (y + x0) - h y";
      
-      txt {* Define $h_0$ as the linear extension of $h$ on $H_0$:*};  
+      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)
+          "\<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$ extend that of
@@ -230,15 +226,13 @@
       qed;
       thus "g ~= graph H0 h0"; by (simp!);
 
-      txt {* Furthermore  $h_0$ is a norm preserving extension 
+      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);
@@ -314,23 +308,24 @@
 
 subsection  {* An alternative formulation of the theorem *};
 
-text {* The following alternative formulation of the 
-Hahn-Banach Theorem uses the fact that for
-real numbers the following inequations are equivalent:
+text {* The following alternative formulation of the Hahn-Banach
+Theorem\label{rabs-HahnBanach} uses the fact that for real numbers the
+following inequations are equivalent:\footnote{This was shown in lemma
+$\idt{rabs{\dsh}ineq{\dsh}iff}$ (see page \pageref{rabs-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}
-(This was shown in lemma $\idt{rabs{\dsh}ineq}$.) *};
+*};
 
 theorem rabs_HahnBanach:
-  "[| is_vectorspace E; is_subspace F E; is_quasinorm E p; 
+  "[| is_vectorspace E; is_subspace F E; is_seminorm E p; 
   is_linearform F f; ALL x:F. rabs (f x) <= p x |]
   ==> EX g. is_linearform E g
           & (ALL x:F. g x = f x)
           & (ALL x:E. rabs (g x) <= p x)";
 proof -; 
-  assume e: "is_vectorspace E" "is_subspace F E" "is_quasinorm E p" 
+  assume e: "is_vectorspace E" "is_subspace F E" "is_seminorm E p" 
             "is_linearform F f"  "ALL x:F. rabs (f x) <= p x";
   have "ALL x:F. f x <= p x"; 
     by (rule rabs_ineq_iff [RS iffD1]);
@@ -352,36 +347,35 @@
 
 subsection {* The Hahn-Banach Theorem for normed spaces *};
 
-text  {* Every continous linear function $f$ on a subspace of $E$, 
-  can be extended to a continous function on $E$ with the same 
-  function norm. *};
+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_continous F norm f |] 
+  is_linearform F f; is_continuous F norm f |] 
   ==> EX g. is_linearform E g
-         & is_continous E norm 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_continous F norm 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 the function $p$ on $E$ as follows:
   \begin{matharray}{l}
-  p\ap x = \fnorm f \cdot \norm x\\
-  % p\ap x = \fnorm f \cdot \fnorm x\\
+  p \ap x = \fnorm f \cdot \norm x\\
   \end{matharray}
   *};
 
   def p == "\<lambda>x. function_norm F norm f * norm x";
   
-  txt{* $p$ is a quasinorm on $E$: *};
+  txt{* $p$ is a seminorm on $E$: *};
 
-  have q: "is_quasinorm E p";
+  have q: "is_seminorm E p";
   proof;
     fix x y a; assume "x:E" "y:E";
 
@@ -393,14 +387,14 @@
       show "0r <= norm x"; ..;
     qed;
 
-    txt{* $p$ is multiplicative: *};
+    txt{* $p$ is absolutely homogenous: *};
 
     show "p (a <*> x) = rabs a * p x";
     proof -; 
       have "p (a <*> x) = function_norm F norm f * norm (a <*> x)";
         by (simp!);
       also; have "norm (a <*> x) = rabs a * norm x"; 
-        by (rule normed_vs_norm_mult_distrib);
+        by (rule normed_vs_norm_rabs_homogenous);
       also; have "function_norm F norm f * (rabs a * norm x) 
         = rabs a * (function_norm F norm f * norm x)";
         by (simp! only: real_mult_left_commute);
@@ -408,7 +402,7 @@
       finally; show ?thesis; .;
     qed;
 
-    txt{* Furthermore, $p$ obeys the triangle inequation: *};
+    txt{* Furthermore, $p$ is subadditive: *};
 
     show "p (x + y) <= p x + p y";
     proof -;
@@ -436,10 +430,10 @@
        by (simp! add: norm_fx_le_norm_f_norm_x);
   qed;
 
-  txt{* Using the facts that $p$ is a quasinorm and 
-  $f$ is bounded we can apply the Hahn-Banach Theorem for real
-  vector spaces. 
-  So $f$ can be extended in a norm preserving way to some function
+  txt{* Using the fact that $p$ is a seminorm and 
+  $f$ is bounded by $q$ 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; 
@@ -451,36 +445,43 @@
   proof (elim exE conjE); 
     fix g;
     assume "is_linearform E g" and a: "ALL x:F. g x = f x" 
-       and "ALL x:E. rabs (g x) <= p x";
+       and b: "ALL x:E. rabs (g x) <= p x";
 
     show "EX g. is_linearform E g 
-            & is_continous E norm 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{* To complete the proof, we show that this function
-    $g$ is also continous and has the same function norm as
-    $f$. *};
+    txt{* We futhermore have to show that 
+    $g$ is also continuous: *};
 
-      show g_cont: "is_continous E norm g";
+      show g_cont: "is_continuous E norm g";
       proof;
         fix x; assume "x:E";
+        from b [RS bspec, OF this]; 
         show "rabs (g x) <= function_norm F norm f * norm x";
-          by (rule bspec [of _ _ x], (simp!));
+          by (unfold p_def);
       qed; 
 
+      txt {* To complete the proof, we show that 
+      $\fnorm g = \fnorm f$. *};
+
       show "function_norm E norm g = function_norm F norm f"
         (is "?L = ?R");
       proof (rule order_antisym);
 
-        txt{* $\idt{function{\dsh}norm}\ap F\ap \idt{norm}\ap f$ is 
-        a solution
-        for the inequation 
+        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}
-        \forall\ap x\in E.\ap |g\ap x| \leq c \cdot \norm x
-        \end{matharray} *};
-
+        \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. rabs (g x) <= function_norm F norm f * norm x";
         proof;
           fix x; assume "x:E"; 
@@ -488,12 +489,7 @@
             by (simp!);
         qed;
 
-        txt{* Since
-         $\idt{function{\dsh}norm}\ap E\ap \idt{norm}\ap g$
-        is the smallest solution for this inequation, we have: *};
-
-        with _ g_cont;
-        show "?L <= ?R";
+        with _ g_cont; show "?L <= ?R";
         proof (rule fnorm_le_ub);
           from f_cont f_norm; show "0r <= function_norm F norm f"; ..;
         qed;
diff -r 67bfcd3a433c -r 1b99ee57d131 src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Fri Oct 29 20:18:34 1999 +0200
@@ -3,88 +3,89 @@
     Author:     Gertrud Bauer, TU Munich
 *)
 
-header {* Extending a non-maximal function *};
+header {* Extending non-maximal functions *};
 
 theory HahnBanachExtLemmas = FunctionNorm:;
 
 text{* In this section the following context is presumed.
 Let $E$ be a real vector space with a 
-quasinorm $q$ on $E$. $F$ is a subspace of $E$ and $f$ a linear 
+seminorm $q$ on $E$. $F$ is a subspace of $E$ and $f$ a linear 
 function on $F$. We consider a subspace $H$ of $E$ that is a 
-superspace of $F$ and a linearform $h$ on $H$. $H$ is a not equal 
+superspace of $F$ and a linear form $h$ on $H$. $H$ is a not equal 
 to $E$ and $x_0$ is an element in $E \backslash H$.
 $H$ is extended to the direct sum  $H_0 = H + \idt{lin}\ap x_0$, so for
 any $x\in H_0$ the decomposition of $x = y + a \mult x$ 
 with $y\in H$ is unique. $h_0$ is defined on $H_0$ by  
-$h_0 x = h y + a \cdot \xi$ for some $\xi$.
+$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 
-extension of $f$. It is a conclusion of the completenesss of the 
-reals. To show 
+text {* This lemma will be used to show the existence of a linear
+extension of $f$ (see page \pageref{ex-xi-use}). 
+It is a consequence
+of the completeness of $\bbbR$. To show 
 \begin{matharray}{l}
-\exists \xi. \ap (\forall y\in F.\ap a\ap y \leq \xi) \land (\forall y\in F.\ap xi \leq b\ap y)
-\end{matharray}
+\Ex{\xi}{\All {y\in F}{a\ap y \leq \xi \land \xi \leq b\ap y}}
+\end{matharray} 
 it suffices to show that 
-\begin{matharray}{l}
-\forall u\in F. \ap\forall v\in F. \ap a\ap u \leq b \ap v
-\end{matharray}
-*};
+\begin{matharray}{l} \All
+{u\in F}{\All {v\in F}{a\ap u \leq b \ap v}} 
+\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) & (ALL y:F. xi <= b y)"; 
+  ==> 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\ap u.\ap u\in F\}$ has a supremum, if
-  it is non-empty and if it has an upperbound. *};
+  it is non-empty and has an upper bound. *};
 
-  let ?S = "{s::real. EX u:F. s = a u}";
+  let ?S = "{a u :: real | u. u:F}";
 
   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 <0> : ?S"; by force;
     thus "EX X. X : ?S"; ..;
 
-    txt {* $b\ap \zero$ is an upperboud 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 <0>)";
       proof (intro isUbI setleI ballI);
+        show "b <0> : 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"; ..;
+        from y; have "EX u:F. y = a u"; by fast;
         thus "y <= b <0>"; 
         proof;
-          fix u; assume "u:F"; assume "y = a u";
+          fix u; assume "u:F"; 
+          assume "y = a u";
           also; have "a u <= b <0>"; by (rule r) (simp!)+;
           finally; show ?thesis; .;
         qed;
-      next;
-        show "b <0> : UNIV"; by simp;
       qed;
     qed;
   qed;
 
-  thus "EX xi. (ALL y:F. a y <= xi) & (ALL y:F. xi <= b y)"; 
+  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";    
@@ -93,16 +94,16 @@
       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"; by simp;
+        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"; ..;
+          hence "EX u:F. au = a u"; by fast;
           thus "au <= b y";
           proof;
             fix u; assume "u:F"; assume "au = a u";  
@@ -115,25 +116,26 @@
   qed;
 qed;
 
-text{* The function $h_0$ is defined as a canonical linear extension
-of $h$ to $H_0$. *};
+text{* The function $h_0$ is defined as a
+$h_0\ap x = h\ap y + a\cdot \xi$ where $x = y + a\prod \xi$
+is a linear extension of $h$ to $H_0$. *};
 
 lemma h0_lf: 
-  "[| h0 = (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H 
+  "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H 
                 in h y + a * xi);
-  H0 = H + lin x0; is_subspace H E; is_linearform H h; x0 ~: H; 
+  H0 == H + lin x0; is_subspace H E; is_linearform H h; x0 ~: H; 
   x0 : E; x0 ~= <0>; 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 <*> 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 ~= <0>" "x0 : E" "is_vectorspace E";
+    and H0_def: "H0 == H + lin x0" 
+    and vs: "is_subspace H E" "is_linearform H h" "x0 ~: H"
+      "x0 ~= <0>" "x0 : E" "is_vectorspace E";
 
   have h0: "is_vectorspace H0"; 
-  proof (simp only: H0_def, rule vs_sum_vs);
+  proof (unfold H0_def, rule vs_sum_vs);
     show "is_subspace (lin x0) E"; ..;
   qed; 
 
@@ -141,8 +143,7 @@
   proof;
     fix x1 x2; assume x1: "x1 : H0" and x2: "x2 : H0"; 
 
-    txt{* We now have to show that $h_0$ is linear 
-    w.~r.~t.~addition, i.~e.\
+    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$. *}; 
 
@@ -150,13 +151,13 @@
       by (rule vs_add_closed, rule h0); 
     from x1; 
     have ex_x1: "EX y1 a1. x1 = y1 + a1 <*> x0  & y1 : H"; 
-      by (simp add: H0_def vs_sum_def lin_def) blast;
+      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 (simp add: H0_def vs_sum_def lin_def) blast;
+      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 (simp add: H0_def vs_sum_def lin_def) force;
+      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";
@@ -167,7 +168,7 @@
          and y: "x1 + x2 = y + a <*> x0"   and y':  "y  : H"; 
 
       have ya: "y1 + y2 = y & a1 + a2 = a"; 
-      proof (rule decomp_H0); 
+      proof (rule decomp_H0);  txt{*\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"; ..;
@@ -179,7 +180,7 @@
         by (simp add: ya);
       also; from vs y1' y2'; 
       have "... = h y1 + h y2 + a1 * xi + a2 * xi"; 
-	by (simp add: linearform_add_linear [of H] 
+	by (simp add: linearform_add [of H] 
                       real_add_mult_distrib);
       also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)"; 
         by simp;
@@ -190,24 +191,23 @@
       finally; show ?thesis; .;
     qed;
  
-    txt{* We further have to show that $h_0$ is linear 
-    w.~r.~t.~scalar multiplication, 
+    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 any real number $c$. 
+    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_x1: "EX y1 a1. x1 = y1 + a1 <*> x0 & y1 : H";
-      by (simp add: H0_def vs_sum_def lin_def) fast;
     from x1; have ex_x: "!! x. x: H0 
                         ==> EX y a. x = y + a <*> x0 & y : H";
-      by (simp add: H0_def vs_sum_def lin_def) fast;
-    note ex_ax1 = ex_x [of "c <*> x1", OF ax1];
+      by (unfold H0_def vs_sum_def lin_def) fast;
 
-    with ex_x1; show "h0 (c <*> x1) = c * (h0 x1)";  
+    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"
@@ -225,7 +225,7 @@
       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_linear [of H]);
+	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"; 
@@ -235,30 +235,31 @@
   qed;
 qed;
 
-text{* $h_0$ is bounded by the quasinorm $p$. *};
+text{* The linear extension $h_0$ of $h$
+is bounded by the seminorm $p$. *};
 
 lemma h0_norm_pres:
-  "[| h0 = (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H 
+  "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H 
                 in h y + a * xi);
-  H0 = H + lin x0; x0 ~: H; x0 : E; x0 ~= <0>; is_vectorspace E; 
-  is_subspace H E; is_quasinorm E p; is_linearform H h; 
+  H0 == H + lin x0; x0 ~: H; x0 : E; x0 ~= <0>; 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) 
   & (ALL y:H. xi <= p (y + x0) - h y) |]
    ==> 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 <*> x0 & y:H 
                in (h y) + a * xi)"
-    and H0_def: "H0 = H + lin x0" 
+    and H0_def: "H0 == H + lin x0" 
     and vs: "x0 ~: H" "x0 : E" "x0 ~= <0>" "is_vectorspace E" 
-            "is_subspace H E" "is_quasinorm E p" "is_linearform H h" 
-    and a:      " ALL y:H. h y <= p y";
-  presume a1: "ALL y:H. - p (y + x0) - h y <= xi";
-  presume a2: "ALL y:H. xi <= p (y + x0) - h y";
+            "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"; 
   have ex_x: 
     "!! x. x : H0 ==> EX y a. x = y + a <*> x0 & y : H";
-    by (simp add: H0_def vs_sum_def lin_def) fast;
+    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";
@@ -268,7 +269,7 @@
       by (rule h0_definite);
 
     txt{* Now we show  
-    $h\ap y + a \cdot xi\leq  p\ap (y\plus a \mult x_0)$ 
+    $h\ap y + a \cdot \xi\leq  p\ap (y\plus a \mult x_0)$ 
     by case analysis on $a$. *};
 
     also; have "... <= p (y + a <*> x0)";
@@ -277,17 +278,17 @@
       assume z: "a = 0r"; 
       with vs y a; show ?thesis; by simp;
 
-    txt {* In the case $a < 0$ we use $a_1$ with $y$ taken as
-    $y/a$. *};
+    txt {* In the case $a < 0$, we use $a_1$ with $\idt{ya}$ 
+    taken as $y/a$: *};
 
     next;
       assume lz: "a < 0r"; hence nz: "a ~= 0r"; by simp;
       from a1; 
       have "- p (rinv a <*> y + x0) - h (rinv a <*> y) <= xi";
-        by (rule bspec)(simp!);
- 
-      txt {* The thesis now follows by a short calculation. *};      
+        by (rule bspec) (simp!);
 
+      txt {* The thesis for this case now follows by a short  
+      calculation. *};      
       hence "a * xi 
             <= a * (- p (rinv a <*> y + x0) - h (rinv a <*> y))";
         by (rule real_mult_less_le_anti [OF lz]);
@@ -296,25 +297,28 @@
         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: quasinorm_mult_distrib rabs_minus_eqI2);
+        by (simp add: seminorm_rabs_homogenous rabs_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_linear [RS sym]);
+        by (simp add: linearform_mult [RS sym]);
       finally; have "a * xi <= p (y + a <*> 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;
 
-      txt {* In the case $a > 0$ we use $a_2$ with $y$ taken
-      as $y/a$. *};
+      txt {* In the case $a > 0$, we use $a_2$ with $\idt{ya}$ 
+      taken as $y/a$: *};
+
     next; 
       assume gz: "0r < a"; hence nz: "a ~= 0r"; by simp;
+      from a2;
       have "xi <= p (rinv a <*> y + x0) - h (rinv a <*> y)";
-        by (rule bspec [OF a2]) (simp!);
+        by (rule bspec) (simp!);
 
-      txt {* The thesis follows by a short calculation. *};
+      txt {* The thesis for this case follows by a short
+      calculation: *};
 
       with gz; have "a * xi 
             <= a * (p (rinv a <*> y + x0) - h (rinv a <*> y))";
@@ -325,12 +329,12 @@
       also; from gz vs y; 
       have "a * p (rinv a <*> y + x0) 
            = p (a <*> (rinv a <*> y + x0))";
-        by (simp add: quasinorm_mult_distrib rabs_eqI2);
+        by (simp add: seminorm_rabs_homogenous rabs_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_linear [RS sym]); 
+        by (simp add: linearform_mult [RS sym]); 
       finally; have "a * xi <= p (y + a <*> x0) - h y"; .;
  
       hence "h y + a * xi <= h y + (p (y + a <*> x0) - h y)";
@@ -342,5 +346,4 @@
   qed;
 qed blast+; 
 
-
 end;
\ No newline at end of file
diff -r 67bfcd3a433c -r 1b99ee57d131 src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Fri Oct 29 20:18:34 1999 +0200
@@ -10,20 +10,20 @@
 
 
 text{* This section contains some lemmas that will be used in the
-proof of the Hahn-Banach theorem.
+proof of the Hahn-Banach Theorem.
 In this section the following context is presumed. 
-Let $E$ be a real vector space with a quasinorm $q$ on $E$. 
-$F$ is a subspace of $E$ and $f$ a linearform on $F$. We 
-consider a chain $c$ of norm preserving extensions of $f$, such that
+Let $E$ be a real vector space with a seminorm $q$ on $E$. 
+$F$ is a subspace of $E$ and $f$ a linear form on $F$. We 
+consider a chain $c$ of norm-preserving extensions of $f$, such that
 $\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$.
+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|]
+  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' 
@@ -60,14 +60,14 @@
 qed;
 ***)
 
-text{* Let $c$ be a chain of norm preserving extensions of the 
+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. *};
 
 lemma some_H'h't:
   "[| M = norm_pres_extensions E p F f; c: chain M; 
-  graph H h = Union c; x:H|]
+  graph H h = Union c; x:H |]
    ==> 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' 
@@ -109,7 +109,7 @@
 qed;
 
 
-text{*  Let $c$ be a chain of norm preserving extensions of the
+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 the domain $H$ of the supremum function is member of
 the domain $H'$ of some function $h'$, such that $h$ extends $h'$.
@@ -117,7 +117,7 @@
 
 lemma some_H'h': 
   "[| M = norm_pres_extensions E p F f; c: chain M; 
-  graph H h = Union c; x:H|] 
+  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)"; 
@@ -147,7 +147,7 @@
 (***
 lemma some_H'h': 
   "[| M = norm_pres_extensions E p F f; c: chain M; 
-  graph H h = Union c; x:H|] 
+  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)"; 
@@ -185,7 +185,7 @@
 
 
 text{* Any two elements $x$ and $y$ in the domain $H$ of the 
-supremum function $h$ lie both in the domain $H'$ of some function 
+supremum function $h$ are both in the domain $H'$ of some function 
 $h'$, such that $h$ extends $h'$. *};
 
 lemma some_H'h'2: 
@@ -265,7 +265,7 @@
 (***
 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|] 
+  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)"; 
@@ -350,7 +350,7 @@
 
     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";
@@ -366,8 +366,8 @@
       fix H1 h1 H2 h2; 
       assume "graph H1 h1 = G1" "graph H2 h2 = G2";
 
-      txt{* Since both h $G_1$ and $G_2$ are members of $c$, 
-      $G_1$ is contained in $G_2$ or vice versa. *};
+      txt{* $G_1$ is contained in $G_2$ or vice versa, 
+      since both $G_1$ and $G_2$ are members of $c$. *};
 
       have "G1 <= G2 | G2 <= G1" (is "?case1 | ?case2"); ..;
       thus ?thesis;
@@ -390,10 +390,10 @@
   qed;
 qed;
 
-text{* The limit function $h$ is linear: every element $x$ in the
+text{* 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 value of $x$ are identical for $h'$ and $h$.  Finally, the
+the function values of $x$ are identical for $h'$ and $h$.  Finally, the
 function $h'$ is linear by construction of $M$.  *};
 
 lemma sup_lf: 
@@ -412,8 +412,7 @@
             & (ALL x:H'. h' x <= p x)";
       by (rule some_H'h'2);
 
-    txt {* We have to show that h is linear w.~r.~t. 
-    addition. *};
+    txt {* We have to show that $h$ is additive. *};
 
     thus "h (x + y) = h x + h y"; 
     proof (elim exE conjE);
@@ -421,7 +420,7 @@
         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_linear);
+        by (rule linearform_add);
       also; have "h' x = h x"; ..;
       also; have "h' y = h y"; ..;
       also; have "x + y : H'"; ..;
@@ -436,8 +435,7 @@
             & (ALL x:H'. h' x <= p x)";
       by (rule some_H'h');
 
-    txt{* We have to show that h is linear w.~r.~t. 
-    scalar multiplication. *};
+    txt{* We have to show that $h$ is multiplicative. *};
 
     thus "h (a <*> x) = a * h x";
     proof (elim exE conjE);
@@ -445,7 +443,7 @@
         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_linear);
+        by (rule linearform_mult);
       also; have "h' x = h x"; ..;
       also; have "a <*> x : H'"; ..;
       with b; have "h' (a <*> x) = h (a <*> x)"; ..;
@@ -462,7 +460,7 @@
 
 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";
+  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";
@@ -484,9 +482,11 @@
 
     thus ?thesis; 
     proof (elim exE conjE); 
-      fix G g; assume "graph G g = x" "graph F f <= graph G g";
-      have "graph F f <= graph G g"; .;
-      also; have "graph G g <= graph H h"; by (simp!, fast);
+      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;
@@ -539,15 +539,15 @@
   show ?thesis; 
   proof;
  
-    txt {* The $\zero$ element lies in $H$, as $F$ is a subset 
-    of $H$. *};
+    txt {* The $\zero$ element is in $H$, as $F$ is a subset 
+    of $H$: *};
 
     have "<0> : F"; ..;
     also; have "is_subspace F H"; by (rule sup_supF); 
     hence "F <= H"; ..;
     finally; show "<0> : H"; .;
 
-    txt{* $H$ is a subset of $E$. *};
+    txt{* $H$ is a subset of $E$: *};
 
     show "H <= E"; 
     proof;
@@ -565,7 +565,7 @@
       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); 
@@ -586,7 +586,7 @@
       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); 
@@ -609,7 +609,8 @@
 qed;
 
 text {* The limit function is bounded by 
-the norm $p$ as well, since all elements in the chain are norm preserving.
+the norm $p$ as well, since all elements in the chain are
+bounded by $p$.
 *};
 
 lemma sup_norm_pres: 
@@ -635,10 +636,10 @@
 qed;
 
 
-text_raw{* \medskip *}
-text{* The following lemma is a property of real linearforms on 
+text{* \medskip The following lemma is a property of linearforms on 
 real vector spaces. It will be used for the lemma 
-$\idt{rabs{\dsh}HahnBanach}$.
+$\idt{rabs{\dsh}HahnBanach}$ (see page \pageref{rabs-HahnBanach}).
+\label{rabs-ineq-iff}
 For real vector spaces the following inequations are equivalent:
 \begin{matharray}{ll} 
 \forall x\in H.\ap |h\ap x|\leq p\ap x& {\rm and}\\ 
@@ -647,12 +648,12 @@
 *};
 
 lemma rabs_ineq_iff: 
-  "[| is_subspace H E; is_vectorspace E; is_quasinorm E p; 
+  "[| is_subspace H E; is_vectorspace E; is_seminorm E p; 
   is_linearform H h |] 
   ==> (ALL x:H. rabs (h x) <= p x) = (ALL x:H. h x <= p x)" 
   (concl is "?L = ?R");
 proof -;
-  assume "is_subspace H E" "is_vectorspace E" "is_quasinorm E p" 
+  assume "is_subspace H E" "is_vectorspace E" "is_seminorm E p" 
          "is_linearform H h";
   have h: "is_vectorspace H"; ..;
   show ?thesis;
@@ -675,10 +676,10 @@
       show "- p x <= h x";
       proof (rule real_minus_le);
 	from h; have "- h x = h (- x)"; 
-          by (rule linearform_neg_linear [RS sym]);
+          by (rule linearform_neg [RS sym]);
 	also; from r; have "... <= p (- x)"; by (simp!);
 	also; have "... = p x"; 
-          by (rule quasinorm_minus, rule subspace_subsetD);
+          by (rule seminorm_minus, rule subspace_subsetD);
 	finally; show "- h x <= p x"; .; 
       qed;
       from r; show "h x <= p x"; ..; 
diff -r 67bfcd3a433c -r 1b99ee57d131 src/HOL/Real/HahnBanach/Linearform.thy
--- a/src/HOL/Real/HahnBanach/Linearform.thy	Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Linearform.thy	Fri Oct 29 20:18:34 1999 +0200
@@ -7,9 +7,8 @@
 
 theory Linearform = VectorSpace:;
 
-text{* A \emph{linearform} is a function on a vector
-space into the reals that is linear w.~r.~t.~addition and skalar
-multiplikation. *};
+text{* A \emph{linear form} is a function on a vector
+space into the reals that is additive and multiplicative. *};
 
 constdefs
   is_linearform :: "['a::{minus, plus} set, 'a => real] => bool" 
@@ -23,38 +22,38 @@
  ==> is_linearform V f";
  by (unfold is_linearform_def) force;
 
-lemma linearform_add_linear [intro!!]: 
+lemma linearform_add [intro!!]: 
   "[| is_linearform V f; x:V; y:V |] ==> f (x + y) = f x + f y";
   by (unfold is_linearform_def) fast;
 
-lemma linearform_mult_linear [intro!!]: 
+lemma linearform_mult [intro!!]: 
   "[| is_linearform V f; x:V |] ==>  f (a <*> x) = a * (f x)"; 
   by (unfold is_linearform_def) fast;
 
-lemma linearform_neg_linear [intro!!]:
+lemma linearform_neg [intro!!]:
   "[|  is_vectorspace V; is_linearform V f; x:V|] 
   ==> f (- x) = - f x";
 proof -; 
   assume "is_linearform V f" "is_vectorspace V" "x:V"; 
   have "f (- x) = f ((- 1r) <*> x)"; by (simp! add: negate_eq1);
-  also; have "... = (- 1r) * (f x)"; by (rule linearform_mult_linear);
+  also; have "... = (- 1r) * (f x)"; by (rule linearform_mult);
   also; have "... = - (f x)"; by (simp!);
   finally; show ?thesis; .;
 qed;
 
-lemma linearform_diff_linear [intro!!]: 
+lemma linearform_diff [intro!!]: 
   "[| is_vectorspace V; is_linearform V f; x:V; y:V |] 
   ==> f (x - y) = f x - f y";  
 proof -;
   assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V";
   have "f (x - y) = f (x + - y)"; by (simp! only: diff_eq1);
   also; have "... = f x + f (- y)"; 
-    by (rule linearform_add_linear) (simp!)+;
-  also; have "f (- y) = - f y"; by (rule linearform_neg_linear);
+    by (rule linearform_add) (simp!)+;
+  also; have "f (- y) = - f y"; by (rule linearform_neg);
   finally; show "f (x - y) = f x - f y"; by (simp!);
 qed;
 
-text{* Every linearform yields $0$ for the $\zero$ vector.*};
+text{* Every linear form yields $0$ for the $\zero$ vector.*};
 
 lemma linearform_zero [intro!!, simp]: 
   "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r"; 
@@ -62,7 +61,7 @@
   assume "is_vectorspace V" "is_linearform V f";
   have "f <0> = f (<0> - <0>)"; by (simp!);
   also; have "... = f <0> - f <0>"; 
-    by (rule linearform_diff_linear) (simp!)+;
+    by (rule linearform_diff) (simp!)+;
   also; have "... = 0r"; by simp;
   finally; show "f <0> = 0r"; .;
 qed; 
diff -r 67bfcd3a433c -r 1b99ee57d131 src/HOL/Real/HahnBanach/NormedSpace.thy
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Fri Oct 29 20:18:34 1999 +0200
@@ -11,60 +11,61 @@
 
 subsection {* Quasinorms *};
 
-text{* A \emph{quasinorm} $\norm{\cdot}$ is a  function on a real vector space into the reals 
-that has the following properties: *};
+text{* A \emph{seminorm} $\norm{\cdot}$ is a function on a real vector
+space into the reals that has the following properties: It is positive
+definite, absolute homogenous and subadditive.  *};
 
 constdefs
-  is_quasinorm :: "['a::{plus, minus} set, 'a => real] => bool"
-  "is_quasinorm V norm == ALL x: V. ALL y:V. ALL a. 
+  is_seminorm :: "['a::{plus, minus} set, 'a => real] => bool"
+  "is_seminorm V norm == ALL x: V. ALL y:V. ALL a. 
         0r <= norm x 
       & norm (a <*> x) = (rabs a) * (norm x)
       & norm (x + y) <= norm x + norm y";
 
-lemma is_quasinormI [intro]: 
-  "[| !! x y a. [| x:V; y:V|] ==>  0r <= norm x;
+lemma is_seminormI [intro]: 
+  "[| !! x y a. [| x:V; y:V|] ==> 0r <= norm x;
   !! x a. x:V ==> norm (a <*> x) = (rabs a) * (norm x);
   !! x y. [|x:V; y:V |] ==> norm (x + y) <= norm x + norm y |] 
-  ==> is_quasinorm V norm";
-  by (unfold is_quasinorm_def, force);
+  ==> is_seminorm V norm";
+  by (unfold is_seminorm_def, force);
 
-lemma quasinorm_ge_zero [intro!!]:
-  "[| is_quasinorm V norm; x:V |] ==> 0r <= norm x";
-  by (unfold is_quasinorm_def, force);
+lemma seminorm_ge_zero [intro!!]:
+  "[| is_seminorm V norm; x:V |] ==> 0r <= norm x";
+  by (unfold is_seminorm_def, force);
 
-lemma quasinorm_mult_distrib: 
-  "[| is_quasinorm V norm; x:V |] 
+lemma seminorm_rabs_homogenous: 
+  "[| is_seminorm V norm; x:V |] 
   ==> norm (a <*> x) = (rabs a) * (norm x)";
-  by (unfold is_quasinorm_def, force);
+  by (unfold is_seminorm_def, force);
 
-lemma quasinorm_triangle_ineq: 
-  "[| is_quasinorm V norm; x:V; y:V |] 
+lemma seminorm_subadditive: 
+  "[| is_seminorm V norm; x:V; y:V |] 
   ==> norm (x + y) <= norm x + norm y";
-  by (unfold is_quasinorm_def, force);
+  by (unfold is_seminorm_def, force);
 
-lemma quasinorm_diff_triangle_ineq: 
-  "[| is_quasinorm V norm; x:V; y:V; is_vectorspace V |] 
+lemma seminorm_diff_subadditive: 
+  "[| is_seminorm V norm; x:V; y:V; is_vectorspace V |] 
   ==> norm (x - y) <= norm x + norm y";
 proof -;
-  assume "is_quasinorm V norm" "x:V" "y:V" "is_vectorspace V";
+  assume "is_seminorm V norm" "x:V" "y:V" "is_vectorspace V";
   have "norm (x - y) = norm (x + - 1r <*> y)";  
     by (simp! add: diff_eq2 negate_eq2);
   also; have "... <= norm x + norm  (- 1r <*> y)"; 
-    by (simp! add: quasinorm_triangle_ineq);
+    by (simp! add: seminorm_subadditive);
   also; have "norm (- 1r <*> y) = rabs (- 1r) * norm y"; 
-    by (rule quasinorm_mult_distrib);
+    by (rule seminorm_rabs_homogenous);
   also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one);
   finally; show "norm (x - y) <= norm x + norm y"; by simp;
 qed;
 
-lemma quasinorm_minus: 
-  "[| is_quasinorm V norm; x:V; is_vectorspace V |] 
+lemma seminorm_minus: 
+  "[| is_seminorm V norm; x:V; is_vectorspace V |] 
   ==> norm (- x) = norm x";
 proof -;
-  assume "is_quasinorm V norm" "x:V" "is_vectorspace V";
-  have "norm (- x) = norm (-1r <*> x)"; by (simp! only: negate_eq1);
-  also; have "... = rabs (-1r) * norm x"; 
-    by (rule quasinorm_mult_distrib);
+  assume "is_seminorm V norm" "x:V" "is_vectorspace V";
+  have "norm (- x) = norm (- 1r <*> x)"; by (simp! only: negate_eq1);
+  also; have "... = rabs (- 1r) * norm x"; 
+    by (rule seminorm_rabs_homogenous);
   also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one);
   finally; show "norm (- x) = norm x"; by simp;
 qed;
@@ -72,20 +73,20 @@
 
 subsection {* Norms *};
 
-text{* A \emph{norm} $\norm{\cdot}$ is a quasinorm that maps only the
+text{* A \emph{norm} $\norm{\cdot}$ is a seminorm that maps only the
 $\zero$ vector to $0$. *};
 
 constdefs
   is_norm :: "['a::{minus, plus} set, 'a => real] => bool"
-  "is_norm V norm == ALL x: V.  is_quasinorm V norm 
+  "is_norm V norm == ALL x: V.  is_seminorm V norm 
       & (norm x = 0r) = (x = <0>)";
 
 lemma is_normI [intro]: 
-  "ALL x: V.  is_quasinorm V norm  & (norm x = 0r) = (x = <0>) 
+  "ALL x: V.  is_seminorm V norm  & (norm x = 0r) = (x = <0>) 
   ==> is_norm V norm"; by (simp only: is_norm_def);
 
-lemma norm_is_quasinorm [intro!!]: 
-  "[| is_norm V norm; x:V |] ==> is_quasinorm V norm";
+lemma norm_is_seminorm [intro!!]: 
+  "[| is_norm V norm; x:V |] ==> is_seminorm V norm";
   by (unfold is_norm_def, force);
 
 lemma norm_zero_iff: 
@@ -94,7 +95,7 @@
 
 lemma norm_ge_zero [intro!!]:
   "[|is_norm V norm; x:V |] ==> 0r <= norm x";
-  by (unfold is_norm_def is_quasinorm_def, force);
+  by (unfold is_norm_def is_seminorm_def, force);
 
 
 subsection {* Normed vector spaces *};
@@ -141,16 +142,16 @@
   finally; show "0r < norm x"; .;
 qed;
 
-lemma normed_vs_norm_mult_distrib [intro!!]: 
+lemma normed_vs_norm_rabs_homogenous [intro!!]: 
   "[| is_normed_vectorspace V norm; x:V |] 
   ==> norm (a <*> x) = (rabs a) * (norm x)";
-  by (rule quasinorm_mult_distrib, rule norm_is_quasinorm, 
+  by (rule seminorm_rabs_homogenous, rule norm_is_seminorm, 
       rule normed_vs_norm);
 
-lemma normed_vs_norm_triangle_ineq [intro!!]: 
+lemma normed_vs_norm_subadditive [intro!!]: 
   "[| is_normed_vectorspace V norm; x:V; y:V |] 
   ==> norm (x + y) <= norm x + norm y";
-  by (rule quasinorm_triangle_ineq, rule norm_is_quasinorm, 
+  by (rule seminorm_subadditive, rule norm_is_seminorm, 
      rule normed_vs_norm);
 
 text{* Any subspace of a normed vector space is again a 
@@ -165,7 +166,7 @@
   show "is_vectorspace F"; ..;
   show "is_norm F norm"; 
   proof (intro is_normI ballI conjI);
-    show "is_quasinorm F norm"; 
+    show "is_seminorm F norm"; 
     proof;
       fix x y a; presume "x : E";
       show "0r <= norm x"; ..;
diff -r 67bfcd3a433c -r 1b99ee57d131 src/HOL/Real/HahnBanach/ROOT.ML
--- a/src/HOL/Real/HahnBanach/ROOT.ML	Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/ROOT.ML	Fri Oct 29 20:18:34 1999 +0200
@@ -5,5 +5,4 @@
 The Hahn-Banach theorem for real vector spaces (Isabelle/Isar).
 *)
 
-time_use_thy "Bounds";
 time_use_thy "HahnBanach";
diff -r 67bfcd3a433c -r 1b99ee57d131 src/HOL/Real/HahnBanach/Subspace.thy
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Fri Oct 29 20:18:34 1999 +0200
@@ -17,15 +17,15 @@
 
 constdefs 
   is_subspace ::  "['a::{minus, plus} set, 'a set] => bool"
-  "is_subspace U V ==  U ~= {}  & U <= V 
-     &  (ALL x:U. ALL y:U. ALL a. x + y : U & a <*> x : U)";
+  "is_subspace U V == U ~= {} & U <= V 
+     & (ALL x:U. ALL y:U. ALL a. x + y : U & a <*> x : U)";
 
 lemma subspaceI [intro]: 
-  "[| <0>:U; U <= V; ALL x:U. ALL y:U. (x + y : U); 
+  "[| <0> : U; U <= V; ALL x:U. ALL y:U. (x + y : U); 
   ALL x:U. ALL a. a <*> x : U |]
   ==> is_subspace U V";
 proof (unfold is_subspace_def, intro conjI); 
-  assume "<0>:U"; thus "U ~= {}"; by fast;
+  assume "<0> : U"; thus "U ~= {}"; by fast;
 qed (simp+);
 
 lemma subspace_not_empty [intro!!]: "is_subspace U V ==> U ~= {}";
@@ -35,28 +35,28 @@
   by (unfold is_subspace_def) simp;
 
 lemma subspace_subsetD [simp, intro!!]: 
-  "[| is_subspace U V; x:U |]==> x:V";
+  "[| is_subspace U V; x:U |] ==> x:V";
   by (unfold is_subspace_def) force;
 
 lemma subspace_add_closed [simp, intro!!]: 
-  "[| is_subspace U V; x: U; y: U |] ==> x + y : U";
+  "[| is_subspace U V; x:U; y:U |] ==> x + y : U";
   by (unfold is_subspace_def) simp;
 
 lemma subspace_mult_closed [simp, intro!!]: 
-  "[| is_subspace U V; x: U |] ==> a <*> x: U";
+  "[| is_subspace U V; x:U |] ==> a <*> x : U";
   by (unfold is_subspace_def) simp;
 
 lemma subspace_diff_closed [simp, intro!!]: 
-  "[| is_subspace U V; is_vectorspace V; x: U; y: U |] 
-  ==> x - y: U";
+  "[| is_subspace U V; is_vectorspace V; x:U; y:U |] 
+  ==> x - y : U";
   by (simp! add: diff_eq1 negate_eq1);
 
 text {* Similar as for linear spaces, the existence of the 
-zero element in every subspace follws from the non-emptyness 
-of the subspace and vector space laws.*};
+zero element in every subspace follows from the non-emptiness 
+of the carrier set and by vector space laws.*};
 
 lemma zero_in_subspace [intro !!]:
-  "[| is_subspace U V; is_vectorspace V |] ==> <0>:U";
+  "[| is_subspace U V; is_vectorspace V |] ==> <0> : U";
 proof -; 
   assume "is_subspace U V" and v: "is_vectorspace V";
   have "U ~= {}"; ..;
@@ -72,11 +72,11 @@
 qed;
 
 lemma subspace_neg_closed [simp, intro!!]: 
-  "[| is_subspace U V; is_vectorspace V; x: U |] ==> - x: U";
+  "[| is_subspace U V; is_vectorspace V; x:U |] ==> - x : U";
   by (simp add: negate_eq1);
 
 text_raw {* \medskip *};
-text {* Further derived laws: Every subspace is a vector space. *};
+text {* Further derived laws: every subspace is a vector space. *};
 
 lemma subspace_vs [intro!!]:
   "[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U";
@@ -84,7 +84,7 @@
   assume "is_subspace U V" "is_vectorspace V";
   show ?thesis;
   proof; 
-    show "<0>:U"; ..;
+    show "<0> : U"; ..;
     show "ALL x:U. ALL a. a <*> x : U"; by (simp!);
     show "ALL x:U. ALL y:U. x + y : U"; by (simp!);
     show "ALL x:U. - x = -1r <*> x"; by (simp! add: negate_eq1);
@@ -134,26 +134,26 @@
 
 subsection {* Linear closure *};
 
-text {* The \emph{linear closure} of a vector $x$ is the set of all 
-multiples of $x$. *};
+text {* The \emph{linear closure} of a vector $x$ is the set of all
+scalar multiples of $x$. *};
 
 constdefs
   lin :: "'a => 'a set"
-  "lin x == {y. EX a. y = a <*> x}";
+  "lin x == {a <*> x | a. True}"; 
 
 lemma linD: "x : lin v = (EX a::real. x = a <*> v)";
-  by (unfold lin_def) force;
+  by (unfold lin_def) fast;
 
 lemma linI [intro!!]: "a <*> x0 : lin x0";
-  by (unfold lin_def) force;
+  by (unfold lin_def) fast;
 
 text {* Every vector is contained in its linear closure. *};
 
-lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x:lin x";
-proof (unfold lin_def, intro CollectI exI);
+lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x : lin x";
+proof (unfold lin_def, intro CollectI exI conjI);
   assume "is_vectorspace V" "x:V";
   show "x = 1r <*> x"; by (simp!);
-qed;
+qed simp;
 
 text {* Any linear closure is a subspace. *};
 
@@ -162,12 +162,12 @@
 proof;
   assume "is_vectorspace V" "x:V";
   show "<0> : lin x"; 
-  proof (unfold lin_def, intro CollectI exI);
+  proof (unfold lin_def, intro CollectI exI conjI);
     show "<0> = 0r <*> x"; by (simp!);
-  qed;
+  qed simp;
 
   show "lin x <= V";
-  proof (unfold lin_def, intro subsetI, elim CollectE exE); 
+  proof (unfold lin_def, intro subsetI, elim CollectE exE conjE); 
     fix xa a; assume "xa = a <*> x"; 
     show "xa:V"; by (simp!);
   qed;
@@ -176,21 +176,23 @@
   proof (intro ballI);
     fix x1 x2; assume "x1 : lin x" "x2 : lin x"; 
     thus "x1 + x2 : lin x";
-    proof (unfold lin_def, elim CollectE exE, intro CollectI exI);
+    proof (unfold lin_def, elim CollectE exE conjE, 
+      intro CollectI exI conjI);
       fix a1 a2; assume "x1 = a1 <*> x" "x2 = a2 <*> x";
       show "x1 + x2 = (a1 + a2) <*> x"; 
         by (simp! add: vs_add_mult_distrib2);
-    qed;
+    qed simp;
   qed;
 
   show "ALL xa:lin x. ALL a. a <*> xa : lin x"; 
   proof (intro ballI allI);
     fix x1 a; assume "x1 : lin x"; 
     thus "a <*> x1 : lin x";
-    proof (unfold lin_def, elim CollectE exE, intro CollectI exI);
+    proof (unfold lin_def, elim CollectE exE conjE,
+      intro CollectI exI conjI);
       fix a1; assume "x1 = a1 <*> x";
       show "a <*> x1 = (a * a1) <*> x"; by (simp!);
-    qed;
+    qed simp;
   qed; 
 qed;
 
@@ -213,7 +215,7 @@
 instance set :: (plus) plus; by intro_classes;
 
 defs vs_sum_def:
-  "U + V == {x. EX u:U. EX v:V. x = u + v}";(***  
+  "U + V == {u + v | u v. u:U & v:V}"; (***
 
 constdefs 
   vs_sum :: 
@@ -223,13 +225,13 @@
 
 lemma vs_sumD: 
   "x: U + V = (EX u:U. EX v:V. x = u + v)";
-  by (unfold vs_sum_def) simp;
+    by (unfold vs_sum_def) fast;
 
 lemmas vs_sumE = vs_sumD [RS iffD1, elimify];
 
 lemma vs_sumI [intro!!]: 
   "[| x:U; y:V; t= x + y |] ==> t : U + V";
-  by (unfold vs_sum_def, intro CollectI bexI); 
+  by (unfold vs_sum_def) fast;
 
 text{* $U$ is a subspace of $U + V$. *};
 
@@ -287,7 +289,7 @@
     qed (simp!)+;
   qed;
 
-  show "ALL x: U + V. ALL a. a <*> x : U + V";
+  show "ALL x : U + V. ALL a. a <*> x : U + V";
   proof (intro ballI allI);
     fix x a; assume "x : U + V";
     thus "a <*> x : U + V";
@@ -348,10 +350,11 @@
   qed;
 qed;
 
-text {* An application of the previous lemma will be used in the 
-proof of the Hahn-Banach theorem: for an element $y + a \mult x_0$ 
-of the direct sum of a vectorspace $H$ and the linear closure of 
-$x_0$ the components $y \in H$ and $a$ are unique. *}; 
+text {* An application of the previous lemma will be used in the proof
+of the Hahn-Banach Theorem (see page \pageref{decomp-H0-use}): for any
+element $y + a \mult x_0$ of the direct sum of a vectorspace $H$ and
+the linear closure of $x_0$ the components $y \in H$ and $a$ are
+uniquely determined. *};
 
 lemma decomp_H0: 
   "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; 
@@ -370,9 +373,9 @@
     proof;
       show "H Int lin x0 <= {<0>}"; 
       proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]);
-        fix x; assume "x:H" "x:lin x0"; 
+        fix x; assume "x:H" "x : lin x0"; 
         thus "x = <0>";
-        proof (unfold lin_def, elim CollectE exE);
+        proof (unfold lin_def, elim CollectE exE conjE);
           fix a; assume "x = a <*> x0";
           show ?thesis;
           proof (rule case_split);
@@ -388,8 +391,9 @@
        qed;
       qed;
       show "{<0>} <= H Int lin x0";
-      proof (intro subsetI, elim singletonE, intro IntI, simp+);
-        show "<0> : H"; ..;
+      proof (intro subsetI, elim singletonE, intro IntI, 
+        (simp only:)+);
+        show "<0>:H"; ..;
         from lin_vs; show "<0> : lin x0"; ..;
       qed;
     qed;
@@ -404,20 +408,20 @@
   qed;
 qed;
 
-text {* Since for an element $y + a \mult x_0$ of the direct sum 
+text {* Since for any element $y + a \mult x_0$ of the direct sum 
 of a vectorspace $H$ and the linear closure of $x_0$ the components
-$y\in H$ and $a$ are unique, follows from $y\in H$ the fact that 
+$y\in H$ and $a$ are unique, it follows from $y\in H$ that 
 $a = 0$.*}; 
 
 lemma decomp_H0_H: 
-  "[| is_vectorspace E; is_subspace H E; t:H; x0~:H; x0:E;
+  "[| is_vectorspace E; is_subspace H E; t:H; x0 ~: H; x0:E;
   x0 ~= <0> |] 
   ==> (SOME (y, a). t = y + a <*> x0 & y : H) = (t, 0r)";
 proof (rule, unfold split_paired_all);
-  assume "is_vectorspace E" "is_subspace H E" "t:H" "x0~:H" "x0:E"
+  assume "is_vectorspace E" "is_subspace H E" "t:H" "x0 ~: H" "x0:E"
     "x0 ~= <0>";
   have h: "is_vectorspace H"; ..;
-  fix y a; presume t1: "t = y + a <*> x0" and "y : H";
+  fix y a; presume t1: "t = y + a <*> x0" and "y:H";
   have "y = t & a = 0r"; 
     by (rule decomp_H0) (assumption | (simp!))+;
   thus "(y, a) = (t, 0r)"; by (simp!);
@@ -428,14 +432,14 @@
 $h_0 (y \plus a \mult x_0) = h y + a \cdot \xi$ is definite. *};
 
 lemma h0_definite:
-  "[| h0 = (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
+  "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
                 in (h y) + a * xi);
   x = y + a <*> x0; is_vectorspace E; is_subspace H E;
   y:H; x0 ~: H; x0:E; x0 ~= <0> |]
   ==> h0 x = h y + a * xi";
 proof -;  
   assume 
-    "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 <*> x0 & y:H)
                in (h y) + a * xi)"
     "x = y + a <*> x0" "is_vectorspace E" "is_subspace H E"
     "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
@@ -443,25 +447,25 @@
     by (simp! add: vs_sum_def lin_def) force+;
   have "EX! xa. ((\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)"; 
   proof;
-    show "EX xa. ((%(y, a). x = y + a <*> x0 & y:H) xa)";
+    show "EX xa. ((\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)";
       by (force!);
   next;
     fix xa ya;
-    assume "(%(y,a). x = y + a <*> x0 & y : H) xa"
-           "(%(y,a). x = y + a <*> x0 & y : H) ya";
+    assume "(\<lambda>(y,a). x = y + a <*> x0 & y : H) xa"
+           "(\<lambda>(y,a). x = y + a <*> x0 & y : H) ya";
     show "xa = ya"; ;
     proof -;
       show "fst xa = fst ya & snd xa = snd ya ==> xa = ya"; 
         by (rule Pair_fst_snd_eq [RS iffD2]);
-      have x: "x = (fst xa) + (snd xa) <*> x0 & (fst xa) : H"; 
+      have x: "x = fst xa + snd xa <*> x0 & fst xa : H"; 
         by (force!);
-      have y: "x = (fst ya) + (snd ya) <*> x0 & (fst ya) : H"; 
+      have y: "x = fst ya + snd ya <*> x0 & fst ya : H"; 
         by (force!);
       from x y; show "fst xa = fst ya & snd xa = snd ya"; 
         by (elim conjE) (rule decomp_H0, (simp!)+);
     qed;
   qed;
-  hence eq: "(SOME (y, a). (x = y + a <*> x0 & y:H)) = (y, a)"; 
+  hence eq: "(SOME (y, a). x = y + a <*> x0 & y:H) = (y, a)"; 
     by (rule select1_equality) (force!);
   thus "h0 x = h y + a * xi"; by (simp! add: Let_def);
 qed;
diff -r 67bfcd3a433c -r 1b99ee57d131 src/HOL/Real/HahnBanach/VectorSpace.thy
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Fri Oct 29 20:18:34 1999 +0200
@@ -10,14 +10,11 @@
 subsection {* Signature *};
 
 text {* For the definition of real vector spaces a type $\alpha$
-of the sort $\idt{plus}, \idt{minus}$ is considered, on which a
-real scalar multiplication $\mult$ is defined, and which has an zero 
-element $\zero$.*};
+of the sort $\{ \idt{plus}, \idt{minus}\}$ is considered, on which a
+real scalar multiplication $\mult$, and a zero 
+element $\zero$ is defined. *};
 
 consts
-(***
-  sum	:: "['a, 'a] => 'a"                         (infixl "+" 65)
-***)
   prod  :: "[real, 'a] => 'a"                       (infixr "<*>" 70)
   zero  :: 'a                                       ("<0>");
 
@@ -45,7 +42,7 @@
   and commutative; $\minus x$ is the inverse of $x$ w.~r.~t.~addition
   and $\zero$ is the neutral element of addition.  Addition and
   multiplication are distributive; scalar multiplication is
-  associative and the real $1$ is the neutral element of scalar
+  associative and the real number $1$ is the neutral element of scalar
   multiplication.
 *};
 
@@ -55,7 +52,7 @@
    & (ALL x:V. ALL y:V. ALL z:V. ALL a b.
         x + y : V                                 
       & a <*> x : V                                 
-      & x + y + z = x + (y + z)             
+      & (x + y) + z = x + (y + z)             
       & x + y = y + x                           
       & x - x = <0>                               
       & <0> + x = x                               
@@ -72,8 +69,8 @@
 lemma vsI [intro]:
   "[| <0>:V; 
   ALL x:V. ALL y:V. x + y : V; 
-  ALL x:V. ALL a. a <*> x : V;    
-  ALL x:V. ALL y:V. ALL z:V. x + y + z = x + (y + z);
+  ALL x:V. ALL a. a <*> x : V;  
+  ALL x:V. ALL y:V. ALL z:V. (x + y) + z = x + (y + z);
   ALL x:V. ALL y:V. x + y = y + x;
   ALL x:V. x - x = <0>;
   ALL x:V. <0> + x = x;
@@ -82,7 +79,7 @@
   ALL x:V. ALL a b. (a * b) <*> x = a <*> b <*> x; 
   ALL x:V. 1r <*> x = x; 
   ALL x:V. - x = (- 1r) <*> x; 
-  ALL x:V. ALL y:V. x - y = x + - y|] ==> is_vectorspace V";
+  ALL x:V. ALL y:V. x - y = x + - y |] ==> is_vectorspace V";
 proof (unfold is_vectorspace_def, intro conjI ballI allI);
   fix x y z; 
   assume "x:V" "y:V" "z:V"
@@ -113,7 +110,7 @@
   by (unfold is_vectorspace_def) simp;
  
 lemma vs_add_closed [simp, intro!!]: 
-  "[| is_vectorspace V; x:V; y:V|] ==> x + y : V"; 
+  "[| is_vectorspace V; x:V; y:V |] ==> x + y : V"; 
   by (unfold is_vectorspace_def) simp;
 
 lemma vs_mult_closed [simp, intro!!]: 
@@ -121,7 +118,7 @@
   by (unfold is_vectorspace_def) simp;
 
 lemma vs_diff_closed [simp, intro!!]: 
- "[| is_vectorspace V; x:V; y:V|] ==> x - y : V";
+ "[| is_vectorspace V; x:V; y:V |] ==> x - y : V";
   by (simp add: diff_eq1 negate_eq1);
 
 lemma vs_neg_closed  [simp, intro!!]: 
@@ -129,8 +126,8 @@
   by (simp add: negate_eq1);
 
 lemma vs_add_assoc [simp]:  
-  "[| is_vectorspace V; x:V; y:V; z:V|]
-   ==> x + y + z = x + (y + z)";
+  "[| is_vectorspace V; x:V; y:V; z:V |]
+   ==> (x + y) + z = x + (y + z)";
   by (unfold is_vectorspace_def) fast;
 
 lemma vs_add_commute [simp]: 
@@ -155,8 +152,8 @@
   "[| is_vectorspace V; x:V |] ==>  x - x = <0>"; 
   by (unfold is_vectorspace_def) simp;
 
-text {* The existence of the zero element a vector space
-follows from the non-emptyness of the vector space. *};
+text {* The existence of the zero element of a vector space
+follows from the non-emptiness of carrier set. *};
 
 lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> <0>:V";
 proof -; 
@@ -228,12 +225,12 @@
   finally; show ?thesis; .;
 qed;
 
-(*text_raw {* \paragraph {Further derived laws:} *};*)
+(*text_raw {* \paragraph {Further derived laws.} *};*)
 text_raw {* \medskip *};
 text{* Further derived laws: *};
 
 lemma vs_mult_zero_left [simp]: 
-  "[| is_vectorspace V; x:V|] ==> 0r <*> x = <0>";
+  "[| is_vectorspace V; x:V |] ==> 0r <*> x = <0>";
 proof -;
   assume "is_vectorspace V" "x:V";
   have  "0r <*> x = (1r - 1r) <*> x"; by (simp only: real_diff_self);
@@ -304,11 +301,11 @@
 qed;
 
 lemma vs_add_minus_cancel [simp]:  
-  "[| is_vectorspace V; x:V; y:V |] ==>  x + (- x + y) = y"; 
+  "[| is_vectorspace V; x:V; y:V |] ==> x + (- x + y) = y"; 
   by (simp add: vs_add_assoc [RS sym] del: vs_add_commute); 
 
 lemma vs_minus_add_cancel [simp]: 
-  "[| is_vectorspace V; x:V; y:V |] ==>  - x + (x + y) = y"; 
+  "[| is_vectorspace V; x:V; y:V |] ==> - x + (x + y) = y"; 
   by (simp add: vs_add_assoc [RS sym] del: vs_add_commute); 
 
 lemma vs_minus_add_distrib [simp]:  
@@ -325,7 +322,7 @@
   by (simp add:diff_eq1);
 
 lemma vs_add_left_cancel:
-  "[| is_vectorspace V; x:V; y:V; z:V|] 
+  "[| is_vectorspace V; x:V; y:V; z:V |] 
    ==> (x + y = x + z) = (y = z)"  
   (concl is "?L = ?R");
 proof;
@@ -338,7 +335,7 @@
   also; have "- x + ... = - x + x + z"; 
     by (rule vs_add_assoc [RS sym]) (simp!)+;
   also; have "... = z"; by (simp!);
-  finally; show ?R;.;
+  finally; show ?R; .;
 qed force;
 
 lemma vs_add_right_cancel: 
@@ -381,7 +378,7 @@
     by (simp! only: vs_mult_assoc);
   also; assume ?L;
   also; have "rinv a <*> ... = y"; by (simp!);
-  finally; show ?R;.;
+  finally; show ?R; .;
 qed simp;
 
 lemma vs_mult_right_cancel: (*** forward ***)
@@ -437,7 +434,7 @@
     also; from vs; have "... = z + <0>"; 
       by (simp only: vs_add_minus_left);
     also; from vs; have "... = z"; by (simp only: vs_add_zero_right);
-    finally; show ?R;.;
+    finally; show ?R; .;
   next;
     assume ?R;
     hence "z - y = (x + y) - y"; by simp;
@@ -451,7 +448,7 @@
 qed;
 
 lemma vs_add_minus_eq_minus: 
-  "[| is_vectorspace V; x:V; y:V; x + y = <0>|] ==> x = - y"; 
+  "[| is_vectorspace V; x:V; y:V; x + y = <0> |] ==> x = - y"; 
 proof -;
   assume "is_vectorspace V" "x:V" "y:V"; 
   have "x = (- y + y) + x"; by (simp!);
@@ -473,11 +470,11 @@
 qed;
 
 lemma vs_add_diff_swap:
-  "[| is_vectorspace V; a:V; b:V; c:V; d:V; a + b = c + d|] 
+  "[| is_vectorspace V; a:V; b:V; c:V; d:V; a + b = c + d |] 
   ==> a - c = d - b";
 proof -; 
   assume vs: "is_vectorspace V" "a:V" "b:V" "c:V" "d:V" 
-  and eq: "a + b = c + d";
+    and eq: "a + b = c + d";
   have "- c + (a + b) = - c + (c + d)"; 
     by (simp! add: vs_add_left_cancel);
   also; have "... = d"; by (rule vs_minus_add_cancel);
@@ -491,9 +488,9 @@
 qed;
 
 lemma vs_add_cancel_21: 
-  "[| is_vectorspace V; x:V; y:V; z:V; u:V|] 
+  "[| is_vectorspace V; x:V; y:V; z:V; u:V |] 
   ==> (x + (y + z) = y + u) = ((x + z) = u)"
-  (concl is "?L = ?R" ); 
+  (concl is "?L = ?R"); 
 proof -; 
   assume "is_vectorspace V" "x:V" "y:V""z:V" "u:V";
   show "?L = ?R";
diff -r 67bfcd3a433c -r 1b99ee57d131 src/HOL/Real/HahnBanach/ZornLemma.thy
--- a/src/HOL/Real/HahnBanach/ZornLemma.thy	Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/ZornLemma.thy	Fri Oct 29 20:18:34 1999 +0200
@@ -8,10 +8,10 @@
 theory ZornLemma = Aux + Zorn:;
 
 text{* 
-Zorn's Lemmas says: if every linear ordered subset of an ordered set 
+Zorn's Lemmas states: if every linear ordered subset of an ordered set 
 $S$ has an upper bound in $S$, then there exists a maximal element in $S$.
-In our application $S$ is a set of sets, ordered by set inclusion. Since 
-the union of a chain of sets is an upperbound for all elements of the 
+In our application, $S$ is a set of sets ordered by set inclusion. Since 
+the union of a chain of sets is an upper bound for all elements of the 
 chain, the conditions of Zorn's lemma can be modified:
 if $S$ is non-empty, it suffices to show that for every non-empty 
 chain $c$ in $S$ the union of $c$ also lies in $S$.
@@ -21,6 +21,8 @@
   "a:S ==> (!!c. c: chain S ==> EX x. x:c ==> Union c : S) 
   ==>  EX y: S. ALL z: S. y <= z --> y = z";
 proof (rule Zorn_Lemma2);
+  txt_raw{* \footnote{See
+  \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Zorn.html}}*};
   assume aS: "a:S";
   assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : S";
   show "ALL c:chain S. EX y:S. ALL z:c. z <= y";
@@ -30,13 +32,13 @@
     proof (rule case_split);
  
       txt{* If $c$ is an empty chain, then every element
-      in $S$ is an upperbound of $c$. *};
+      in $S$ is an upper bound of $c$. *};
 
       assume "c={}"; 
       with aS; show ?thesis; by fast;
 
       txt{* If $c$ is non-empty, then $\Union c$ 
-      is an upperbound of $c$, that lies in $S$. *};
+      is an upper bound of $c$, lying in $S$. *};
 
     next;
       assume c: "c~={}";
diff -r 67bfcd3a433c -r 1b99ee57d131 src/HOL/Real/HahnBanach/document/bbb.sty
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/HahnBanach/document/bbb.sty	Fri Oct 29 20:18:34 1999 +0200
@@ -0,0 +1,25 @@
+% bbb.sty  10-Nov-1991, 27-Mar-1994
+%
+% blackboard-bold symbols: B C D E F G H I J K L M N O P Q R T U Z
+%
+
+\def\bbbB{{{\rm I}\mkern-3.8mu{\rm B}}}
+\def\bbbC{{{\rm C}\mkern-15mu{\phantom{\rm t}\vrule}\mkern9mu}}
+\def\bbbD{{{\rm I}\mkern-3.8mu{\rm D}}}
+\def\bbbE{{{\rm I}\mkern-3.8mu{\rm E}}}
+\def\bbbF{{{\rm I}\mkern-3.8mu{\rm F}}}
+\def\bbbG{{{\rm G}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
+\def\bbbH{{{\rm I}\mkern-3.8mu{\rm H}}}
+\def\bbbI{{{\rm I}\mkern-12mu{\phantom{\rm t}\vrule}\mkern6mu}}
+\def\bbbJ{{{\rm J}\mkern-12mu{\phantom{\rm t}\vrule}\mkern6mu}}
+\def\bbbK{{{\rm I}\mkern-3.8mu{\rm K}}}
+\def\bbbL{{{\rm I}\mkern-3.8mu{\rm L}}}
+\def\bbbM{{{\rm I}\mkern-3.8mu{\rm M}}}
+\def\bbbN{{{\rm I}\mkern-3.8mu{\rm N}}}
+\def\bbbO{{{\rm O}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
+\def\bbbP{{{\rm I}\mkern-3.8mu{\rm P}}}
+\def\bbbQ{{{\rm Q}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
+\def\bbbR{{{\rm I}\mkern-3.8mu{\rm R}}}
+\def\bbbT{{{\rm T}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
+\def\bbbU{{{\rm U}\mkern-15mu{\phantom{\rm t}\vrule}\mkern9mu}}
+\def\bbbZ{{{\sf Z}\mkern-7.5mu{\sf Z}}}
diff -r 67bfcd3a433c -r 1b99ee57d131 src/HOL/Real/HahnBanach/document/notation.tex
--- a/src/HOL/Real/HahnBanach/document/notation.tex	Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/document/notation.tex	Fri Oct 29 20:18:34 1999 +0200
@@ -1,11 +1,10 @@
 
 \renewcommand{\isamarkupheader}[1]{\section{#1}}
-\newcommand{\isasymbollambda}{${\mathtt{\lambda}}$}
-
+\newcommand{\isasymlambda}{${\mathtt{\lambda}}$}
+\newcommand{\isasymprod}{\emph{$\mult$}}
+\newcommand{\isasymzero}{\emph{$\zero$}}
 
 
-\newcommand{\name}[1]{\textsf{#1}}
-
 \newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
 \newcommand{\var}[1]{{?\!#1}}
 \DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
@@ -13,30 +12,22 @@
 
 \newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]}
 
-\newcommand{\ty}{{\mathbin{:\,}}}
 \newcommand{\To}{\to}
 \newcommand{\dt}{{\mathpunct.}}
-\newcommand{\all}[1]{\forall #1\dt\;}
-\newcommand{\ex}[1]{\exists #1\dt\;}
-\newcommand{\EX}[1]{\exists #1\dt\;}
-\newcommand{\eps}[1]{\epsilon\; #1}
-%\newcommand{\Forall}{\mathop\bigwedge}
+\newcommand{\Ex}[1]{\exists #1\dt\;}
 \newcommand{\Forall}{\forall}
 \newcommand{\All}[1]{\Forall #1\dt\;}
-\newcommand{\ALL}[1]{\Forall #1\dt\;}
-\newcommand{\Eps}[1]{\Epsilon #1\dt\;}
 \newcommand{\Eq}{\mathbin{\,\equiv\,}}
-\newcommand{\True}{\name{true}}
-\newcommand{\False}{\name{false}}
 \newcommand{\Impl}{\Rightarrow}
 \newcommand{\And}{\;\land\;}
 \newcommand{\Or}{\;\lor\;}
 \newcommand{\Le}{\le}
 \newcommand{\Lt}{\lt}
 \newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
-\newcommand{\ap}{\mathbin{}}
+\newcommand{\ap}{\mathpalette{\mathbin{\!}}{\mathbin{\!}}{\mathbin{}}{\mathbin{}}}
 \newcommand{\Union}{\bigcup}
-
+\newcommand{\Un}{\cup}
+\newcommand{\Int}{\cap}
 
 \newcommand{\norm}[1]{\left\|#1\right\|}
 \newcommand{\fnorm}[1]{\left\|#1\right\|}
@@ -44,20 +35,8 @@
 \newcommand{\plus}{\mathbin{\mathbf +}}
 \newcommand{\minus}{\mathbin{\mathbf -}}
 \newcommand{\mult}{\mathbin{\mathbf\odot}}
-\newcommand{\1}{\mathord{\mathrm{1}}}
-%\newcommand{\zero}{{\mathord{\small\sl\tt {<0>}}}}
-%\newcommand{\plus}{{\mathbin{\;\small\sl\tt {[+]}\;}}}
-%\newcommand{\minus}{{\mathbin{\;\small\sl\tt {[-]}\;}}}
-%\newcommand{\mult}{{\mathbin{\;\small\sl\tt {[*]}\;}}}
-%\newcommand{\1}{{\mathord{\mathrb{1}}}}
-\newcommand{\fl}{{\mathord{\bf\underline{\phantom{i}}}}}
-\renewcommand{\times}{\;{\mathbin{\cdot}}\;}
-\newcommand{\qed}{\hfill~$\Box$}
 
-\newcommand{\isasymbolprod}{$\mult$}
-\newcommand{\isasymbolzero}{$\zero$}
-
-%%% Local Variables: 
+%%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"
-%%% End: 
+%%% End:
diff -r 67bfcd3a433c -r 1b99ee57d131 src/HOL/Real/HahnBanach/document/root.tex
--- a/src/HOL/Real/HahnBanach/document/root.tex	Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/document/root.tex	Fri Oct 29 20:18:34 1999 +0200
@@ -4,6 +4,7 @@
 \usepackage{comment}
 \usepackage{latexsym,theorem}
 \usepackage{isabelle,pdfsetup} %last one!
+\usepackage{bbb}
 
 \input{notation}
 
@@ -13,11 +14,13 @@
 \pagenumbering{arabic}
 
 \title{The Hahn-Banach Theorem for Real Vector Spaces}
-\author{Gertrud Bauer}
+
+\author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}}
+\maketitle
 \maketitle
 
 \begin{abstract}
-  The Hahn-Banach theorem is one of the most fundamental results in functional
+  The Hahn-Banach Theorem is one of the most fundamental results in functional
   analysis. We present a fully formal proof of two versions of the theorem,
   one for general linear spaces and another for normed spaces.  This
   development is based on simply-typed classical set-theory, as provided by
@@ -31,11 +34,11 @@
 \clearpage
 \section{Preface}
 
-This is a fully formal proof of the Hahn-Banach theorem. It closely follows
+This is a fully formal proof of the Hahn-Banach Theorem. It closely follows
 the informal presentation given in the textbook \cite[\S 36]{Heuser:1986}.
 Another formal proof of the same theorem has been done in Mizar
 \cite{Nowak:1993}.  A general overview of the relevance and history of the
-Hahn-Banach theorem is given in \cite{Narici:1996}.
+Hahn-Banach Theorem is given in \cite{Narici:1996}.
 
 \medskip The document is structured as follows.  The first part contains
 definitions of basic notions of linear algebra: vector spaces, subspaces,