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/Library/Target_Numeral.thy
changeset 47159 978c00c20a59
parent 47108 2a1953f0d20d
child 47217 501b9bbd0d6e 
--- a/src/HOL/Library/Target_Numeral.thy	Tue Mar 27 14:49:56 2012 +0200
+++ b/src/HOL/Library/Target_Numeral.thy	Tue Mar 27 15:27:49 2012 +0200
@@ -296,7 +296,7 @@
   have aux2: "\<And>q::int. - int_of k = int_of l * q \<longleftrightarrow> int_of k = int_of l * - q" by auto
   show ?thesis
     by (simp add: prod_eq_iff Target_Numeral.int_eq_iff prod_case_beta aux1)
-      (auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if zdiv_zminus2 zmod_zminus2 aux2)
+      (auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right aux2)
 qed
 
 lemma div_int_code [code]:
isabelle