Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Equiv_Relations.thy
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)
isabelle