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 1155 928a16e02f9f
parent 930 63f02d32509e
child 1401 0c439768f45c 
--- a/src/ZF/WF.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/WF.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -23,8 +23,8 @@
   (*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}))))"
+  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))"
isabelle