--- a/src/ZF/Induct/Acc.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Induct/Acc.thy Tue Mar 06 16:46:27 2012 +0000
@@ -36,7 +36,7 @@
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)
@@ -55,7 +55,7 @@
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