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;