--- a/src/HOL/Real/HahnBanach/Zorn_Lemma.thy Fri Oct 22 18:41:00 1999 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-(* Title: HOL/Real/HahnBanach/Zorn_Lemma.thy
- ID: $Id$
- Author: Gertrud Bauer, TU Munich
-*)
-
-header {* Zorn's Lemma *};
-
-theory Zorn_Lemma = Aux + Zorn:;
-
-lemma Zorn's_Lemma:
- "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);
- 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";
- proof;
- fix c; assume "c:chain S";
-
- show "EX y:S. ALL z:c. z <= y";
- proof (rule case_split [of "c={}"]);
- assume "c={}";
- with aS; show ?thesis; by fast;
- 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;
\ No newline at end of file