author | lcp |
Fri, 14 Apr 1995 11:26:22 +0200 | |
changeset 1058 | b0ff6010602a |
parent 1057 | 5097aa914449 |
child 1059 | 6ad22ffb188b |
--- a/src/ZF/AC/WO6_WO1.thy Fri Apr 14 11:25:23 1995 +0200 +++ b/src/ZF/AC/WO6_WO1.thy Fri Apr 14 11:26:22 1995 +0200 @@ -6,13 +6,6 @@ From the book "Equivalents of the Axiom of Choice" by Rubin & Rubin, pages 2-5 - - - vv1_def "vv1(f,m,b) == if(f`b ~= 0, \ -\ domain(uu(f, b, thing(f,b,g,d), \ -\ LEAST d. domain(uu(f, b, thing(f,b,g,d), d)) ~= 0 & \ -\ domain(uu(f,b, thing(f,b,g,d), d)) lepoll m)), 0)" - *) WO6_WO1 = "rel_is_fun" + AC_Equiv + Let +