Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/WF.thy
changeset 3840 e0baea4d485a
parent 2469 b50b8c0eec01
child 13165 31d020705aff 
--- a/src/ZF/WF.thy	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/WF.thy	Fri Oct 10 18:23:31 1997 +0200
@@ -26,7 +26,7 @@
   is_recfun_def  "is_recfun(r,a,H,f) == 
                         (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))"
+  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))"
isabelle