src/HOL/Real/HahnBanach/Zorn_Lemma.thy
 changeset 7566 c5a3f980a7af parent 7535 599d3414b51d child 7656 2f18c0ffc348
```     1.1 --- a/src/HOL/Real/HahnBanach/Zorn_Lemma.thy	Tue Sep 21 17:30:55 1999 +0200
1.2 +++ b/src/HOL/Real/HahnBanach/Zorn_Lemma.thy	Tue Sep 21 17:31:20 1999 +0200
1.3 @@ -1,5 +1,9 @@
1.4 +(*  Title:      HOL/Real/HahnBanach/Zorn_Lemma.thy
1.5 +    ID:         \$Id\$
1.6 +    Author:     Gertrud Bauer, TU Munich
1.7 +*)
1.8
1.9 -theory Zorn_Lemma = Zorn:;
1.10 +theory Zorn_Lemma = Aux + Zorn:;
1.11
1.12
1.13  lemma Zorn's_Lemma: "a:S ==> (!!c. c: chain S ==> EX x. x:c ==> Union c : S) ==>
1.14 @@ -15,12 +19,12 @@
1.15      show "EX y:S. ALL z:c. z <= y";
1.16      proof (rule case [of "c={}"]);
1.17        assume "c={}";
1.18 -      show ?thesis; by fast;
1.19 +      show ?thesis; by (fast!);
1.20      next;
1.21        assume "c~={}";
1.22        show ?thesis;
1.23        proof;
1.24 -        have "EX x. x:c"; by fast;
1.25 +        have "EX x. x:c"; by (fast!);
1.26          thus "Union c : S"; by (rule s);
1.27          show "ALL z:c. z <= Union c"; by fast;
1.28        qed;
```