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~={}";