src/HOL/Equiv_Relations.thy
changeset 15392 290bc97038c7
parent 15303 eedbb8d22ca2
child 15539 333a88244569
     1.1 --- a/src/HOL/Equiv_Relations.thy	Thu Dec 09 16:45:46 2004 +0100
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Thu Dec 09 18:30:59 2004 +0100
     1.3 @@ -316,8 +316,8 @@
     1.4    apply (rule Union_quotient [THEN subst])
     1.5     apply assumption
     1.6    apply (rule dvd_partition)
     1.7 -     prefer 4 apply (blast dest: quotient_disj)
     1.8 -    apply (simp_all add: Union_quotient equiv_type finite_quotient)
     1.9 +     prefer 3 apply (blast dest: quotient_disj)
    1.10 +    apply (simp_all add: Union_quotient equiv_type)
    1.11    done
    1.12  
    1.13  lemma card_quotient_disjoint: