# HG changeset patch
# User wenzelm
# Date 937927811 -7200
# Node ID 90455fa8cebe91ab988a079e09e7917ea7b6da79
# Parent  26ca52846865649c9fcc0a64f37571e1e9c53dff
Main;

diff -r 26ca52846865 -r 90455fa8cebe src/HOL/Real/Hyperreal/Zorn.thy
--- a/src/HOL/Real/Hyperreal/Zorn.thy	Tue Sep 21 17:29:46 1999 +0200
+++ b/src/HOL/Real/Hyperreal/Zorn.thy	Tue Sep 21 17:30:11 1999 +0200
@@ -5,7 +5,7 @@
     Description : Zorn's Lemma -- See lcp's Zorn.thy in ZF
 *) 
 
-Zorn = Finite +  
+Zorn = Main +  
 
 constdefs
   chain     ::  'a set => 'a set set