--- a/src/ZF/ZF.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/ZF.thy Thu Jan 03 21:15:52 2019 +0100
@@ -7,14 +7,14 @@
subsection\<open>Iteration of the function @{term F}\<close>
-consts iterates :: "[i=>i,i,i] => i" ("(_^_ '(_'))" [60,1000,1000] 60)
+consts iterates :: "[i=>i,i,i] => i" (\<open>(_^_ '(_'))\<close> [60,1000,1000] 60)
primrec
"F^0 (x) = x"
"F^(succ(n)) (x) = F(F^n (x))"
definition
- iterates_omega :: "[i=>i,i] => i" ("(_^\<omega> '(_'))" [60,1000] 60) where
+ iterates_omega :: "[i=>i,i] => i" (\<open>(_^\<omega> '(_'))\<close> [60,1000] 60) where
"F^\<omega> (x) == \<Union>n\<in>nat. F^n (x)"
lemma iterates_triv: