src/HOL/Real/HahnBanach/ZornLemma.thy

--- a/src/HOL/Real/HahnBanach/ZornLemma.thy	Sun Jun 04 00:09:04 2000 +0200
+++ b/src/HOL/Real/HahnBanach/ZornLemma.thy	Sun Jun 04 19:39:29 2000 +0200
@@ -3,9 +3,9 @@
     Author:     Gertrud Bauer, TU Munich
 *)
 
-header {* Zorn's Lemma *};
+header {* Zorn's Lemma *}
 
-theory ZornLemma = Aux + Zorn:;
+theory ZornLemma = Aux + Zorn:
 
 text {* 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
@@ -13,43 +13,43 @@
 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$. *};
+non-empty chain $c$ in $S$ the union of $c$ also lies in $S$. *}
 
 theorem Zorn's_Lemma: 
   "(!!c. c: chain S ==> EX x. x:c ==> Union c : S) ==> a:S
-  ==>  EX y: S. ALL z: S. y <= z --> y = z";
-proof (rule Zorn_Lemma2);
+  ==>  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}} \isanewline *};
-  assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : S";
-  assume aS: "a:S";
-  show "ALL c:chain S. EX y:S. ALL z:c. z <= y";
-  proof;
-    fix c; assume "c:chain S"; 
-    show "EX y:S. ALL z:c. z <= y";
-    proof cases;
+  \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Zorn.html}} \isanewline *}
+  assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : S"
+  assume aS: "a:S"
+  show "ALL c:chain S. EX y:S. ALL z:c. z <= y"
+  proof
+    fix c assume "c:chain S" 
+    show "EX y:S. ALL z:c. z <= y"
+    proof cases
  
       txt{* If $c$ is an empty chain, then every element
-      in $S$ is an upper bound of $c$. *};
+      in $S$ is an upper bound of $c$. *}
 
-      assume "c={}"; 
-      with aS; show ?thesis; by fast;
+      assume "c={}" 
+      with aS show ?thesis by fast
 
       txt{* If $c$ is non-empty, then $\Union c$ 
-      is an upper bound of $c$, lying in $S$. *};
+      is an upper bound of $c$, lying in $S$. *}
 
-    next;
-      assume c: "c~={}";
-      show ?thesis; 
-      proof; 
-        show "ALL z:c. z <= Union c"; by fast;
-        show "Union c : S"; 
-        proof (rule r);
-          from c; show "EX x. x:c"; by fast;  
-        qed;
-      qed;
-    qed;
-  qed;
-qed;
+    next
+      assume c: "c~={}"
+      show ?thesis 
+      proof 
+        show "ALL z:c. z <= Union c" by fast
+        show "Union c : S" 
+        proof (rule r)
+          from c show "EX x. x:c" by fast  
+        qed
+      qed
+    qed
+  qed
+qed
 
-end;
+end
\ No newline at end of file