src/HOL/Groups_Big.thy
changeset 56166 9a241bc276cd
parent 55096 916b2ac758f4
child 56536 aefb4a8da31f
     1.1 --- a/src/HOL/Groups_Big.thy	Sat Mar 15 16:54:32 2014 +0100
     1.2 +++ b/src/HOL/Groups_Big.thy	Sun Mar 16 18:09:04 2014 +0100
     1.3 @@ -162,8 +162,7 @@
     1.4  proof cases
     1.5    assume "finite C"
     1.6    from UNION_disjoint [OF this assms]
     1.7 -  show ?thesis
     1.8 -    by (simp add: SUP_def)
     1.9 +  show ?thesis by simp
    1.10  qed (auto dest: finite_UnionD intro: infinite)
    1.11  
    1.12  lemma distrib:
    1.13 @@ -1020,7 +1019,7 @@
    1.14     (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
    1.15     ==> card (Union C) = setsum card C"
    1.16  apply (frule card_UN_disjoint [of C id])
    1.17 -apply (simp_all add: SUP_def id_def)
    1.18 +apply simp_all
    1.19  done
    1.20  
    1.21