1.1 --- a/src/HOL/Finite_Set.thy	Sun Jul 20 22:05:35 2014 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Mon Jul 21 17:51:11 2014 +0200
     1.3 @@ -733,6 +733,11 @@
     1.4    then show ?thesis by simp
     1.5  qed
     1.6  
     1.7 +lemma fold_set_union_disj:
     1.8 +  assumes "finite A" "finite B" "A \<inter> B = {}"
     1.9 +  shows "Finite_Set.fold f z (A \<union> B) = Finite_Set.fold f (Finite_Set.fold f z A) B"
    1.10 +using assms(2,1,3) by induction simp_all
    1.11 +
    1.12  end
    1.13  
    1.14  text{* Other properties of @{const fold}: *}