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 15392 290bc97038c7
parent 15303 eedbb8d22ca2
child 15539 333a88244569 
--- a/src/HOL/Equiv_Relations.thy	Thu Dec 09 16:45:46 2004 +0100
+++ b/src/HOL/Equiv_Relations.thy	Thu Dec 09 18:30:59 2004 +0100
@@ -316,8 +316,8 @@
   apply (rule Union_quotient [THEN subst])
    apply assumption
   apply (rule dvd_partition)
-     prefer 4 apply (blast dest: quotient_disj)
-    apply (simp_all add: Union_quotient equiv_type finite_quotient)
+     prefer 3 apply (blast dest: quotient_disj)
+    apply (simp_all add: Union_quotient equiv_type)
   done
 
 lemma card_quotient_disjoint:
isabelle