added both cancel_div_mod_procs
authorhaftmann
Fri Apr 17 08:34:51 2009 +0200 (2009-04-17)
changeset 30939207ec81543f6
parent 30938 c6c9359e474c
child 30940 663af91c0720
added both cancel_div_mod_procs
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/mir_tac.ML
     1.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Thu Apr 16 14:10:58 2009 +0200
     1.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Fri Apr 17 08:34:51 2009 +0200
     1.3 @@ -76,7 +76,7 @@
     1.4  				  @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
     1.5  				  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_arith
     2.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Thu Apr 16 14:10:58 2009 +0200
     2.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Fri Apr 17 08:34:51 2009 +0200
     2.3 @@ -99,7 +99,7 @@
     2.4                                    @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
     2.5                                    @{thm "Suc_plus1"}]
     2.6                          addsimps @{thms add_ac}
     2.7 -                        addsimprocs [cancel_div_mod_proc]
     2.8 +                        addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
     2.9      val simpset0 = HOL_basic_ss
    2.10        addsimps [mod_div_equality', Suc_plus1]
    2.11        addsimps comp_ths