src/ZF/Main.thy

--- a/src/ZF/Main.thy	Thu Jul 18 15:21:42 2002 +0200
+++ b/src/ZF/Main.thy	Fri Jul 19 13:28:19 2002 +0200
@@ -40,6 +40,9 @@
       ==> Ord(F^n (x))"  
 by (induct n rule: nat_induct, simp_all)
 
+lemma iterates_commute: "n \<in> nat ==> F(F^n (x)) = F^n (F(x))"
+by (induct_tac n, simp_all)
+
 
 (* belongs to theory IntDiv *)
 lemmas posDivAlg_induct = posDivAlg_induct [consumes 2]