src/ZF/WF.thy

--- a/src/ZF/WF.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/WF.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -24,7 +24,7 @@
     "wf(r) == \<forall>Z. Z=0 | (\<exists>x\<in>Z. \<forall>y. <y,x>:r \<longrightarrow> ~ y \<in> Z)"
 
 definition
-  wf_on        :: "[i,i]=>o"                      ("wf[_]'(_')")  where
+  wf_on        :: "[i,i]=>o"                      (\<open>wf[_]'(_')\<close>)  where
     (*r is well-founded on A*)
     "wf_on(A,r) == wf(r \<inter> A*A)"
 
@@ -46,7 +46,7 @@
     "wfrec(r,a,H) == wftrec(r^+, a, %x f. H(x, restrict(f,r-``{x})))"
 
 definition
-  wfrec_on     :: "[i, i, i, [i,i]=>i] =>i"       ("wfrec[_]'(_,_,_')")  where
+  wfrec_on     :: "[i, i, i, [i,i]=>i] =>i"       (\<open>wfrec[_]'(_,_,_')\<close>)  where
     "wfrec[A](r,a,H) == wfrec(r \<inter> A*A, a, H)"