src/ZF/AC/WO6_WO1.thy
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 6068 2d8f3e1f1151
     1.1 --- a/src/ZF/AC/WO6_WO1.thy	Mon Feb 05 21:33:14 1996 +0100
     1.2 +++ b/src/ZF/AC/WO6_WO1.thy	Tue Feb 06 12:27:17 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	ZF/AC/WO6_WO1.thy
     1.5 +(*  Title:      ZF/AC/WO6_WO1.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Krzysztof Grabczewski
     1.8 +    Author:     Krzysztof Grabczewski
     1.9  
    1.10  The proof of "WO6 ==> WO1".
    1.11  
    1.12 @@ -20,18 +20,18 @@
    1.13  defs
    1.14  
    1.15    NN_def  "NN(y) == {m:nat. EX a. EX f. Ord(a) & domain(f)=a  &  
    1.16 -			    (UN b<a. f`b) = y & (ALL b<a. f`b lepoll m)}"
    1.17 +                            (UN b<a. f`b) = y & (ALL b<a. f`b lepoll m)}"
    1.18  
    1.19    uu_def  "uu(f, beta, gamma, delta) == (f`beta * f`gamma) Int f`delta"
    1.20  
    1.21    (*Definitions for case 1*)
    1.22  
    1.23 -  vv1_def "vv1(f,m,b) ==   						
    1.24 -   	   let g = LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 &	
    1.25 -	                           domain(uu(f,b,g,d)) lepoll m));   	
    1.26 -	       d = LEAST d. domain(uu(f,b,g,d)) ~= 0 &   		
    1.27 -                           domain(uu(f,b,g,d)) lepoll m		
    1.28 -	   in  if(f`b ~= 0, domain(uu(f,b,g,d)), 0)"
    1.29 +  vv1_def "vv1(f,m,b) ==                                                
    1.30 +           let g = LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 & 
    1.31 +                                   domain(uu(f,b,g,d)) lepoll m));      
    1.32 +               d = LEAST d. domain(uu(f,b,g,d)) ~= 0 &                  
    1.33 +                           domain(uu(f,b,g,d)) lepoll m         
    1.34 +           in  if(f`b ~= 0, domain(uu(f,b,g,d)), 0)"
    1.35  
    1.36    ww1_def "ww1(f,m,b) == f`b - vv1(f,m,b)"
    1.37  
    1.38 @@ -40,7 +40,7 @@
    1.39    (*Definitions for case 2*)
    1.40  
    1.41    vv2_def "vv2(f,b,g,s) ==   
    1.42 -	   if(f`g ~= 0, {uu(f, b, g, LEAST d. uu(f,b,g,d) ~= 0)`s}, 0)"
    1.43 +           if(f`g ~= 0, {uu(f, b, g, LEAST d. uu(f,b,g,d) ~= 0)`s}, 0)"
    1.44  
    1.45    ww2_def "ww2(f,b,g,s) == f`g - vv2(f,b,g,s)"
    1.46