src/HOL/Library/Code_Target_Nat.thy
changeset 66808 1907167b6038
parent 66190 a41435469559
child 68028 1f9f973eed2a
     1.1 --- a/src/HOL/Library/Code_Target_Nat.thy	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/HOL/Library/Code_Target_Nat.thy	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -95,7 +95,7 @@
     1.4  
     1.5  lemma [code]:
     1.6    "Divides.divmod_nat m n = (m div n, m mod n)"
     1.7 -  by (fact divmod_nat_div_mod)
     1.8 +  by (fact divmod_nat_def)
     1.9  
    1.10  lemma [code]:
    1.11    "divmod m n = map_prod nat_of_integer nat_of_integer (divmod m n)"
    1.12 @@ -130,7 +130,7 @@
    1.13  proof -
    1.14    from div_mult_mod_eq have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
    1.15    show ?thesis
    1.16 -    by (simp add: Let_def divmod_nat_div_mod of_nat_add [symmetric])
    1.17 +    by (simp add: Let_def divmod_nat_def of_nat_add [symmetric])
    1.18        (simp add: * mult.commute of_nat_mult add.commute)
    1.19  qed
    1.20