--- a/src/ZF/AC/recfunAC16.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/AC/recfunAC16.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/AC/recfunAC16.thy
+(* Title: ZF/AC/recfunAC16.thy
ID: $Id$
- Author: Krzysztof Grabczewski
+ Author: Krzysztof Grabczewski
A recursive definition used in the proof of WO2 ==> AC16
*)
@@ -15,9 +15,9 @@
recfunAC16_def
"recfunAC16(f,fa,i,a) ==
- transrec2(i, 0,
- %g r. if(EX y:r. fa`g <= y, r,
- r Un {f`(LEAST i. fa`g <= f`i &
- (ALL b<a. (fa`b <= f`i --> (ALL t:r. ~ fa`b <= t))))}))"
+ transrec2(i, 0,
+ %g r. if(EX y:r. fa`g <= y, r,
+ r Un {f`(LEAST i. fa`g <= f`i &
+ (ALL b<a. (fa`b <= f`i --> (ALL t:r. ~ fa`b <= t))))}))"
end