src/ZF/Zorn.thy
changeset 753 ec86863e87c8
parent 578 efc648d29dd0
child 806 6330ca0a3ac5
--- a/src/ZF/Zorn.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Zorn.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -19,7 +19,7 @@
   chain, maxchain :: "i=>i"
   super           :: "[i,i]=>i"
 
-rules
+defs
   Subset_rel_def "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}"
   increasing_def "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}"