src/HOL/Library/Numeral_Type.thy
changeset 33361 1f18de40b43f
parent 33035 15eab423e573
child 35115 446c5063e4fd
--- a/src/HOL/Library/Numeral_Type.thy	Fri Oct 30 13:59:52 2009 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Fri Oct 30 14:00:43 2009 +0100
@@ -188,7 +188,7 @@
 by (rule type_definition.Abs_inverse [OF type])
 
 lemma Rep_Abs_mod: "Rep (Abs (m mod n)) = m mod n"
-by (simp add: Abs_inverse IntDiv.pos_mod_conj [OF size0])
+by (simp add: Abs_inverse pos_mod_conj [OF size0])
 
 lemma Rep_Abs_0: "Rep (Abs 0) = 0"
 by (simp add: Abs_inverse size0)