src/HOL/Decision_Procs/mir_tac.ML
changeset 30939 207ec81543f6
parent 30509 e19d5b459a61
child 31240 2c20bcd70fbe
     1.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Thu Apr 16 14:10:58 2009 +0200
     1.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Fri Apr 17 08:34:51 2009 +0200
     1.3 @@ -99,7 +99,7 @@
     1.4                                    @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
     1.5                                    @{thm "Suc_plus1"}]
     1.6                          addsimps @{thms add_ac}
     1.7 -                        addsimprocs [cancel_div_mod_proc]
     1.8 +                        addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
     1.9      val simpset0 = HOL_basic_ss
    1.10        addsimps [mod_div_equality', Suc_plus1]
    1.11        addsimps comp_ths