src/ZF/Zorn.thy

--- a/src/ZF/Zorn.thy	Thu Apr 22 11:02:22 2004 +0200
+++ b/src/ZF/Zorn.thy	Thu Apr 22 12:11:17 2004 +0200
@@ -19,12 +19,12 @@
   chain      :: "i=>i"
    "chain(A)      == {F \<in> Pow(A). \<forall>X\<in>F. \<forall>Y\<in>F. X<=Y | Y<=X}"
 
+  super      :: "[i,i]=>i"
+   "super(A,c)    == {d \<in> chain(A). c<=d & c\<noteq>d}"
+
   maxchain   :: "i=>i"
    "maxchain(A)   == {c \<in> chain(A). super(A,c)=0}"
 
-  super      :: "[i,i]=>i"
-   "super(A,c)    == {d \<in> chain(A). c<=d & c\<noteq>d}"
-
 
 constdefs
   increasing :: "i=>i"