diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/Finite.thy
--- a/src/ZF/Finite.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Finite.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -183,7 +183,7 @@
 
 lemma FiniteFun_Collect_iff:
      "f \<in> FiniteFun(A, {y:B. P(y)})
-      <-> f \<in> FiniteFun(A,B) & (\<forall>x\<in>domain(f). P(f`x))"
+      \<longleftrightarrow> f \<in> FiniteFun(A,B) & (\<forall>x\<in>domain(f). P(f`x))"
 apply auto
 apply (blast intro: FiniteFun_mono [THEN [2] rev_subsetD])
 apply (blast dest: Pair_mem_PiD FiniteFun_is_fun)