src/ZF/Constructible/Rec_Separation.thy

         (\<forall>j[M]. j\<in>n \<longrightarrow>
           (\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M].
             fun_apply(M,f,j,fj) \<and> successor(M,j,sj) \<and>
             fun_apply(M,f,sj,fsj) \<and> pair(M,fj,fsj,ffp) \<and> ffp \<in> r)))"*)
 definition
-  rtran_closure_mem_fm :: "[i,i,i]=>i" where
+  rtran_closure_mem_fm :: "[i,i,i]\<Rightarrow>i" where
  "rtran_closure_mem_fm(A,r,p) \<equiv>
    Exists(Exists(Exists(
     And(omega_fm(2),
      And(Member(1,2),
       And(succ_fm(1,0),

 
 (*  "rtran_closure(M,r,s) \<equiv>
         \<forall>A[M]. is_field(M,r,A) \<longrightarrow>
          (\<forall>p[M]. p \<in> s \<longleftrightarrow> rtran_closure_mem(M,A,r,p))" *)
 definition
-  rtran_closure_fm :: "[i,i]=>i" where
+  rtran_closure_fm :: "[i,i]\<Rightarrow>i" where
   "rtran_closure_fm(r,s) \<equiv>
    Forall(Implies(field_fm(succ(r),0),
                   Forall(Iff(Member(0,succ(succ(s))),
                              rtran_closure_mem_fm(1,succ(succ(r)),0)))))"
 

 subsubsection\<open>Transitive Closure of a Relation, Internalized\<close>
 
 (*  "tran_closure(M,r,t) \<equiv>
          \<exists>s[M]. rtran_closure(M,r,s) \<and> composition(M,r,s,t)" *)
 definition
-  tran_closure_fm :: "[i,i]=>i" where
+  tran_closure_fm :: "[i,i]\<Rightarrow>i" where
   "tran_closure_fm(r,s) \<equiv>
    Exists(And(rtran_closure_fm(succ(r),0), composition_fm(succ(r),0,succ(s))))"
 
 lemma tran_closure_type [TC]:
      "\<lbrakk>x \<in> nat; y \<in> nat\<rbrakk> \<Longrightarrow> tran_closure_fm(x,y) \<in> formula"

 subsubsection\<open>The Formula \<^term>\<open>is_nth\<close>, Internalized\<close>
 
 (* "is_nth(M,n,l,Z) \<equiv>
       \<exists>X[M]. is_iterates(M, is_tl(M), l, n, X) \<and> is_hd(M,X,Z)" *)
 definition
-  nth_fm :: "[i,i,i]=>i" where
+  nth_fm :: "[i,i,i]\<Rightarrow>i" where
     "nth_fm(n,l,Z) \<equiv> 
        Exists(And(is_iterates_fm(tl_fm(1,0), succ(l), succ(n), 0), 
               hd_fm(0,succ(Z))))"
 
 lemma nth_fm_type [TC]: