--- 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";