src/HOL/IntDiv.thy
changeset 24630 351a308ab58d
parent 24490 a4c2a0ffa5be
child 24993 92dfacb32053
     1.1 --- a/src/HOL/IntDiv.thy	Tue Sep 18 11:06:22 2007 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Tue Sep 18 16:08:00 2007 +0200
     1.3 @@ -530,7 +530,7 @@
     1.4  fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
     1.5    if n = 0 then NONE
     1.6    else
     1.7 -    let val (k, l) = IntInf.divMod (m, n);
     1.8 +    let val (k, l) = Integer.div_mod m n;
     1.9          fun mk_num x = HOLogic.mk_number HOLogic.intT x;
    1.10      in SOME (rule OF [prove ctxt (t == plus (mult u (mk_num k)) (mk_num l))])
    1.11      end);