src/HOL/Groups_Big.thy

   assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {}"
   shows "F g (Union C) = F (F g) C"
 proof cases
   assume "finite C"
   from UNION_disjoint [OF this assms]
-  show ?thesis
-    by (simp add: SUP_def)
+  show ?thesis by simp
 qed (auto dest: finite_UnionD intro: infinite)
 
 lemma distrib:
   "F (\<lambda>x. g x * h x) A = F g A * F h A"
   using assms by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute)

 lemma card_Union_disjoint:
   "finite C ==> (ALL A:C. finite A) ==>
    (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
    ==> card (Union C) = setsum card C"
 apply (frule card_UN_disjoint [of C id])
-apply (simp_all add: SUP_def id_def)
+apply simp_all
 done
 
 
 subsubsection {* Cardinality of products *}