--- a/src/ZF/WF.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/WF.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/wf.thy
+(* Title: ZF/wf.thy
ID: $Id$
- Author: Tobias Nipkow and Lawrence C Paulson
+ Author: Tobias Nipkow and Lawrence C Paulson
Copyright 1994 University of Cambridge
Well-founded Recursion
@@ -9,26 +9,26 @@
WF = Trancl + "mono" + "equalities" +
consts
wf :: i=>o
- wf_on :: [i,i]=>o ("wf[_]'(_')")
+ wf_on :: [i,i]=>o ("wf[_]'(_')")
wftrec,wfrec :: [i, i, [i,i]=>i] =>i
- wfrec_on :: [i, i, i, [i,i]=>i] =>i ("wfrec[_]'(_,_,_')")
+ wfrec_on :: [i, i, i, [i,i]=>i] =>i ("wfrec[_]'(_,_,_')")
is_recfun :: [i, i, [i,i]=>i, i] =>o
the_recfun :: [i, i, [i,i]=>i] =>i
defs
(*r is a well-founded relation*)
- wf_def "wf(r) == ALL Z. Z=0 | (EX x:Z. ALL y. <y,x>:r --> ~ y:Z)"
+ wf_def "wf(r) == ALL Z. Z=0 | (EX x:Z. ALL y. <y,x>:r --> ~ y:Z)"
(*r is well-founded relation over A*)
wf_on_def "wf_on(A,r) == wf(r Int A*A)"
is_recfun_def "is_recfun(r,a,H,f) ==
- (f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))"
+ (f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))"
the_recfun_def "the_recfun(r,a,H) == (THE f.is_recfun(r,a,H,f))"
- wftrec_def "wftrec(r,a,H) == H(a, the_recfun(r,a,H))"
+ wftrec_def "wftrec(r,a,H) == H(a, the_recfun(r,a,H))"
(*public version. Does not require r to be transitive*)
wfrec_def "wfrec(r,a,H) == wftrec(r^+, a, %x f. H(x, restrict(f,r-``{x})))"