changeset 66801 | f3fda9777f9a |
parent 66190 | a41435469559 |
child 66806 | a4e82b58d833 |
--- a/src/HOL/Code_Numeral.thy Sun Oct 08 22:28:19 2017 +0200 +++ b/src/HOL/Code_Numeral.thy Sun Oct 08 22:28:20 2017 +0200 @@ -446,11 +446,11 @@ where "divmod_integer k l = (k div l, k mod l)" -lemma fst_divmod [simp]: +lemma fst_divmod_integer [simp]: "fst (divmod_integer k l) = k div l" by (simp add: divmod_integer_def) -lemma snd_divmod [simp]: +lemma snd_divmod_integer [simp]: "snd (divmod_integer k l) = k mod l" by (simp add: divmod_integer_def)