# HG changeset patch
# User lcp
# Date 797851582 -7200
# Node ID b0ff6010602a8c1c55f69b46cbb31613dc3d2bc4
# Parent  5097aa91444984d49068caca8e2b31a76d486423
Deleted comment

diff -r 5097aa914449 -r b0ff6010602a src/ZF/AC/WO6_WO1.thy
--- 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 +