--- a/src/ZF/AC/WO6_WO1.thy Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/AC/WO6_WO1.thy Thu Jan 07 10:56:05 1999 +0100
@@ -31,19 +31,20 @@
domain(uu(f,b,g,d)) lepoll m));
d = LEAST d. domain(uu(f,b,g,d)) ~= 0 &
domain(uu(f,b,g,d)) lepoll m
- in if(f`b ~= 0, domain(uu(f,b,g,d)), 0)"
+ in if f`b ~= 0 then domain(uu(f,b,g,d)) else 0"
ww1_def "ww1(f,m,b) == f`b - vv1(f,m,b)"
- gg1_def "gg1(f,a,m) == lam b:a++a. if (b<a, vv1(f,m,b), ww1(f,m,b--a))"
+ gg1_def "gg1(f,a,m) == lam b:a++a. if b<a then vv1(f,m,b) else ww1(f,m,b--a)"
(*Definitions for case 2*)
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)"
+ if f`g ~= 0 then {uu(f, b, g, LEAST d. uu(f,b,g,d) ~= 0)`s} else 0"
ww2_def "ww2(f,b,g,s) == f`g - vv2(f,b,g,s)"
- gg2_def "gg2(f,a,b,s) == lam g:a++a. if (g<a, vv2(f,b,g,s), ww2(f,b,g--a,s))"
+ gg2_def "gg2(f,a,b,s) ==
+ lam g:a++a. if g<a then vv2(f,b,g,s) else ww2(f,b,g--a,s)"
end