--- a/src/ZF/AC/WO6_WO1.thy Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/WO6_WO1.thy Mon May 21 14:45:52 2001 +0200
@@ -19,32 +19,32 @@
defs
- 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)}"
+ NN_def "NN(y) == {m \\<in> nat. \\<exists>a. \\<exists>f. Ord(a) & domain(f)=a &
+ (\\<Union>b<a. f`b) = y & (\\<forall>b<a. f`b lepoll m)}"
uu_def "uu(f, beta, gamma, delta) == (f`beta * f`gamma) Int f`delta"
(*Definitions for case 1*)
vv1_def "vv1(f,m,b) ==
- let g = LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 &
+ let g = LEAST g. (\\<exists>d. Ord(d) & (domain(uu(f,b,g,d)) \\<noteq> 0 &
domain(uu(f,b,g,d)) lepoll m));
- d = LEAST d. domain(uu(f,b,g,d)) ~= 0 &
+ d = LEAST d. domain(uu(f,b,g,d)) \\<noteq> 0 &
domain(uu(f,b,g,d)) lepoll m
- in if f`b ~= 0 then domain(uu(f,b,g,d)) else 0"
+ in if f`b \\<noteq> 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 then vv1(f,m,b) else ww1(f,m,b--a)"
+ gg1_def "gg1(f,a,m) == \\<lambda>b \\<in> 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 then {uu(f, b, g, LEAST d. uu(f,b,g,d) ~= 0)`s} else 0"
+ if f`g \\<noteq> 0 then {uu(f, b, g, LEAST d. uu(f,b,g,d) \\<noteq> 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 then vv2(f,b,g,s) else ww2(f,b,g--a,s)"
+ \\<lambda>g \\<in> a++a. if g<a then vv2(f,b,g,s) else ww2(f,b,g--a,s)"
end