src/HOL/Decision_Procs/cooper_tac.ML
changeset 43594 ef1ddc59b825
parent 42368 3b8498ac2314
child 44121 44adaa6db327
     1.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Wed Jun 29 16:31:50 2011 +0200
     1.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Wed Jun 29 17:35:46 2011 +0200
     1.3 @@ -82,7 +82,7 @@
     1.4            @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
     1.5            Suc_eq_plus1]
     1.6        addsimps @{thms add_ac}
     1.7 -      addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
     1.8 +      addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
     1.9      val simpset0 = HOL_basic_ss
    1.10        addsimps [mod_div_equality', Suc_eq_plus1]
    1.11        addsimps comp_arith