src/HOL/IntDiv.thy
changeset 26101 a657683e902a
parent 26086 3c243098b64a
child 26480 544cef16045b
     1.1 --- a/src/HOL/IntDiv.thy	Wed Feb 20 14:52:34 2008 +0100
     1.2 +++ b/src/HOL/IntDiv.thy	Wed Feb 20 14:52:38 2008 +0100
     1.3 @@ -274,13 +274,13 @@
     1.4    val prove_eq_sums =
     1.5      let
     1.6        val simps = @{thm diff_int_def} :: Int_Numeral_Simprocs.add_0s @ @{thms zadd_ac}
     1.7 -    in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end;
     1.8 +    in ArithData.prove_conv all_tac (ArithData.simp_all_tac simps) end;
     1.9  end)
    1.10  
    1.11  in
    1.12  
    1.13 -val cancel_zdiv_zmod_proc = NatArithUtils.prep_simproc
    1.14 -  ("cancel_zdiv_zmod", ["(m::int) + n"], K CancelDivMod.proc)
    1.15 +val cancel_zdiv_zmod_proc = Simplifier.simproc @{theory}
    1.16 +  "cancel_zdiv_zmod" ["(m::int) + n"] (K CancelDivMod.proc)
    1.17  
    1.18  end;
    1.19