src/HOL/Code_Numeral.thy
changeset 60868 dd18c33c001e
parent 60758 d8d85a8172b5
child 61076 bdc1e2f0a86a
     1.1 --- a/src/HOL/Code_Numeral.thy	Thu Aug 06 23:56:48 2015 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Sat Aug 08 10:51:33 2015 +0200
     1.3 @@ -512,9 +512,9 @@
     1.4    "integer_of_int k = (if k < 0 then - (integer_of_int (- k))
     1.5       else if k = 0 then 0
     1.6       else let
     1.7 -       (l, j) = divmod_int k 2;
     1.8 -       l' = 2 * integer_of_int l
     1.9 -     in if j = 0 then l' else l' + 1)"
    1.10 +       l = 2 * integer_of_int (k div 2);
    1.11 +       j = k mod 2
    1.12 +     in if j = 0 then l else l + 1)"
    1.13    by (auto simp add: split_def Let_def integer_eq_iff zmult_div_cancel)
    1.14  
    1.15  hide_const (open) Pos Neg sub dup divmod_abs