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}"