src/ZF/Induct/Acc.thy

 lemma acc_downward: "[| b \<in> acc(r);  <a,b>: r |] ==> a \<in> acc(r)"
   by (erule acc.cases) blast
 
 lemma acc_induct [consumes 1, case_names vimage, induct set: acc]:
     "[| a \<in> acc(r);
-        !!x. [| x \<in> acc(r);  \<forall>y. <y,x>:r --> P(y) |] ==> P(x)
+        !!x. [| x \<in> acc(r);  \<forall>y. <y,x>:r \<longrightarrow> P(y) |] ==> P(x)
      |] ==> P(a)"
   by (erule acc.induct) (blast intro: acc.intros)
 
 lemma wf_on_acc: "wf[acc(r)](r)"
   apply (rule wf_onI2)

   apply (rule subsetI)
   apply (erule wf_induct2, assumption)
    apply (blast intro: accI)+
   done
 
-lemma wf_acc_iff: "wf(r) <-> field(r) \<subseteq> acc(r)"
+lemma wf_acc_iff: "wf(r) \<longleftrightarrow> field(r) \<subseteq> acc(r)"
   by (rule iffI, erule acc_wfD, erule acc_wfI)
 
 end