src/HOL/Real/Hyperreal/Zorn.thy
changeset 7564 90455fa8cebe
parent 7219 4e3f386c2e37
child 9279 fb4186e20148
     1.1 --- a/src/HOL/Real/Hyperreal/Zorn.thy	Tue Sep 21 17:29:46 1999 +0200
     1.2 +++ b/src/HOL/Real/Hyperreal/Zorn.thy	Tue Sep 21 17:30:11 1999 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4      Description : Zorn's Lemma -- See lcp's Zorn.thy in ZF
     1.5  *) 
     1.6  
     1.7 -Zorn = Finite +  
     1.8 +Zorn = Main +  
     1.9  
    1.10  constdefs
    1.11    chain     ::  'a set => 'a set set