changeset 26791 | 3581a9c71909 |
parent 25482 | 4ed49eccb1eb |
child 28229 | 4f06fae6a55e |
--- a/src/HOL/Equiv_Relations.thy Tue May 06 23:33:05 2008 +0200 +++ b/src/HOL/Equiv_Relations.thy Wed May 07 10:56:33 2008 +0200 @@ -316,7 +316,7 @@ lemma equiv_imp_dvd_card: "finite A ==> equiv A r ==> \<forall>X \<in> A//r. k dvd card X ==> k dvd card A" - apply (rule Union_quotient [THEN subst]) + apply (rule Union_quotient [THEN subst [where P="\<lambda>A. k dvd card A"]]) apply assumption apply (rule dvd_partition) prefer 3 apply (blast dest: quotient_disj)