--- a/src/HOL/Groups_Big.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Groups_Big.thy Sun Mar 16 18:09:04 2014 +0100
@@ -162,8 +162,7 @@
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:
@@ -1020,7 +1019,7 @@
(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