diff -r 240509babf00 -r 3ba9be497c33 src/ZF/func.thy
--- a/src/ZF/func.thy	Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/func.thy	Tue Jul 02 13:28:08 2002 +0200
@@ -415,7 +415,7 @@
 
 (*For Finite.ML.  Inclusion of right into left is easy*)
 lemma cons_fun_eq:
-     "c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})"
+     "c ~: A ==> cons(c,A) -> B = (\<Union>f \<in> A->B. \<Union>b\<in>B. {cons(<c,b>, f)})"
 apply (rule equalityI)
 apply (safe elim!: fun_extend3)
 (*Inclusion of left into right*)
@@ -432,6 +432,9 @@
 apply (erule consE, simp_all)
 done
 
+lemma succ_fun_eq: "succ(n) -> B = (\<Union>f \<in> n->B. \<Union>b\<in>B. {cons(<n,b>, f)})"
+by (simp add: succ_def mem_not_refl cons_fun_eq)
+
 ML
 {*
 val Pi_iff = thm "Pi_iff";