--- a/src/ZF/ZF.thy Tue Sep 27 17:03:23 2022 +0100
+++ b/src/ZF/ZF.thy Tue Sep 27 17:46:52 2022 +0100
@@ -7,14 +7,14 @@
subsection\<open>Iteration of the function \<^term>\<open>F\<close>\<close>
-consts iterates :: "[i=>i,i,i] => i" (\<open>(_^_ '(_'))\<close> [60,1000,1000] 60)
+consts iterates :: "[i\<Rightarrow>i,i,i] \<Rightarrow> 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" (\<open>(_^\<omega> '(_'))\<close> [60,1000] 60) where
+ iterates_omega :: "[i\<Rightarrow>i,i] \<Rightarrow> i" (\<open>(_^\<omega> '(_'))\<close> [60,1000] 60) where
"F^\<omega> (x) \<equiv> \<Union>n\<in>nat. F^n (x)"
lemma iterates_triv:
@@ -45,7 +45,7 @@
three cases of ordinals\<close>
definition
- transrec3 :: "[i, i, [i,i]=>i, [i,i]=>i] =>i" where
+ transrec3 :: "[i, i, [i,i]\<Rightarrow>i, [i,i]\<Rightarrow>i] \<Rightarrow>i" where
"transrec3(k, a, b, c) \<equiv>
transrec(k, \<lambda>x r.
if x=0 then a