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
```