# HG changeset patch
# User lcp
# Date 797163574 -7200
# Node ID 0df2af5cba40eb578cc90615a873c19ad938b8f2
# Parent  6a402dc505cfac4cb9de58f5773bd4afefaafb3b
Moved some local definitions to WO6_WO1.ML

diff -r 6a402dc505cf -r 0df2af5cba40 src/ZF/AC/AC_Equiv.thy
--- a/src/ZF/AC/AC_Equiv.thy	Thu Apr 06 12:17:40 1995 +0200
+++ b/src/ZF/AC/AC_Equiv.thy	Thu Apr 06 12:19:34 1995 +0200
@@ -32,16 +32,6 @@
   pairwise_disjoint       :: "i => o"
   sets_of_size_between    :: "[i, i, i] => o"
 
-(* Auxiliary definitions used in proofs *)
-  NN                      :: "i => i"
-  uu                      :: "[i, i, i, i] => i"
-  
-(* Other useful definitions *)
-  vv1                     :: "[i, i, i] => i"
-  ww1                     :: "[i, i, i] => i"
-  vv2                     :: "[i, i, i, i] => i"
-  ww2                     :: "[i, i, i, i] => i"
-
   GG                      :: "[i, i, i] => i"
   GG2                     :: "[i, i, i] => i"
   HH                      :: "[i, i, i] => i"
@@ -150,32 +140,6 @@
   
 (* Auxiliary definitions used in proofs *)
 
-  NN_def                  "NN(y) == {m:nat. EX a. EX f. Ord(a) & domain(f)=a \
-\			   & (UN b<a. f`b) = y & (ALL b<a. f`b lepoll m)}"
-
-  uu_def                  "uu(f, beta, gamma, delta)   \
-\			   == (f`beta * f`gamma) Int f`delta"
-  
-(* Other useful definitions *)
-
-  vv1_def "vv1(f,b,m) == if(f`b ~= 0,   \
-\          domain(uu(f,b,   \
-\          LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 &   \
-\	   domain(uu(f,b,g,d)) lesspoll m)),   \
-\          LEAST d. domain(uu(f,b,   \
-\          LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 &   \
-\	   domain(uu(f,b,g,d)) lesspoll m)), d)) ~= 0 &   \
-\          domain(uu(f,b,   \
-\          LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 &   \
-\	   domain(uu(f,b,g,d)) lesspoll m)), d)) lesspoll m)), 0)"
-
-  ww1_def "ww1(f,b,m) == f`b - vv1(f,b,m)"
-
-  vv2_def "vv2(f,b,g,s) ==   \
-\	   if(f`g ~= 0, {uu(f,b,g,LEAST d. uu(f,b,g,d) ~= 0)`s}, 0)"
-
-  ww2_def "ww2(f,b,g,s) == f`g - vv2(f,b,g,s)"
-
   GG_def  "GG(f,x,a)  == transrec(a, %b r. (lam z:Pow(x).   \
 \	                 if(z=0, x, f`z))`(x - {r`c. c:b}))"