src/HOL/Tools/Qelim/presburger.ML
changeset 30936 d13cecf4ed4c
parent 30699 08760e217eb7
child 31790 05c92381363c
     1.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Thu Apr 16 14:02:12 2009 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Thu Apr 16 14:02:13 2009 +0200
     1.3 @@ -131,7 +131,7 @@
     1.4       @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, 
     1.5       @{thm "mod_1"}, @{thm "Suc_plus1"}]
     1.6    @ @{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 splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits 
    1.10       [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, 
    1.11        @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]