| 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)