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/Divides.thy
changeset 67118 ccab07d1196c
parent 67091 1393c2340eec
child 67226 ec32cdaab97b 
--- a/src/HOL/Divides.thy	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Divides.thy	Sat Dec 02 16:50:53 2017 +0000
@@ -384,7 +384,7 @@
     by (cases l rule: int_cases3)
       (auto simp del: of_nat_mult of_nat_add
         simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
-        eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff)
+        eucl_rel_int_iff divide_int_def modulo_int_def)
 next
   case (neg n)
   then show ?thesis
@@ -392,7 +392,7 @@
     by (cases l rule: int_cases3)
       (auto simp del: of_nat_mult of_nat_add
         simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
-        eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff)
+        eucl_rel_int_iff divide_int_def modulo_int_def)
 qed
 
 lemma divmod_int_unique:
@@ -1155,7 +1155,7 @@
   with that have "int (m mod q) = int (n mod q) \<longleftrightarrow> int q dvd int (m - n)"
     by (simp only: of_nat_mod of_nat_diff)
   then show ?thesis
-    by (simp add: zdvd_int)
+    by simp
 qed
 
 lemma mod_eq_nat1E:
isabelle