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/Number_Theory/Cong.thy
changeset 59010 ec2b4270a502
parent 58937 49e8115f70d8
child 59667 651ea265d568 
--- a/src/HOL/Number_Theory/Cong.thy	Mon Nov 17 14:55:33 2014 +0100
+++ b/src/HOL/Number_Theory/Cong.thy	Mon Nov 17 14:55:34 2014 +0100
@@ -820,7 +820,7 @@
         apply (drule (1) bspec)
         apply (erule conjE)
         apply assumption
-        apply (rule dvd_setprod)
+        apply rule
         using fin a apply auto
         done
       finally show ?thesis
@@ -863,7 +863,7 @@
     apply (rule cong_dvd_modulus_nat)
     apply (rule cong_mod_nat)
     using prodnz apply auto
-    apply (rule dvd_setprod)
+    apply rule
     apply (rule fin)
     apply assumption
     done
isabelle