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 81125 ec121999a9cb
parent 76419 f20865ad6319 
--- a/src/ZF/WF.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/ZF/WF.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -24,7 +24,7 @@
     "wf(r) \<equiv> \<forall>Z. Z=0 | (\<exists>x\<in>Z. \<forall>y. \<langle>y,x\<rangle>:r \<longrightarrow> \<not> y \<in> Z)"
 
 definition
-  wf_on        :: "[i,i]\<Rightarrow>o"                      (\<open>wf[_]'(_')\<close>)  where
+  wf_on :: "[i,i]\<Rightarrow>o"  (\<open>(\<open>open_block notation=\<open>mixfix wf_on\<close>\<close>wf[_]'(_'))\<close>)  where
     (*r is well-founded on A*)
     "wf_on(A,r) \<equiv> wf(r \<inter> A*A)"
 
@@ -46,8 +46,8 @@
     "wfrec(r,a,H) \<equiv> wftrec(r^+, a, \<lambda>x f. H(x, restrict(f,r-``{x})))"
 
 definition
-  wfrec_on     :: "[i, i, i, [i,i]\<Rightarrow>i] \<Rightarrow>i"       (\<open>wfrec[_]'(_,_,_')\<close>)  where
-    "wfrec[A](r,a,H) \<equiv> wfrec(r \<inter> A*A, a, H)"
+  wfrec_on :: "[i, i, i, [i,i]\<Rightarrow>i] \<Rightarrow>i"  (\<open>(\<open>open_block notation=\<open>mixfix wfrec_on\<close>\<close>wfrec[_]'(_,_,_'))\<close>)
+  where "wfrec[A](r,a,H) \<equiv> wfrec(r \<inter> A*A, a, H)"
 
 
 subsection\<open>Well-Founded Relations\<close>
isabelle