# HG changeset patch
# User haftmann
# Date 1239883333 -7200
# Node ID d13cecf4ed4c0117aef6d63fc48a628c9493758f
# Parent  db5dcc1f276d02b3d20038f96bcf03a12ba097a1
added simproc

diff -r db5dcc1f276d -r d13cecf4ed4c src/HOL/Tools/Qelim/presburger.ML
--- a/src/HOL/Tools/Qelim/presburger.ML	Thu Apr 16 14:02:12 2009 +0200
+++ b/src/HOL/Tools/Qelim/presburger.ML	Thu Apr 16 14:02:13 2009 +0200
@@ -131,7 +131,7 @@
      @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, 
      @{thm "mod_1"}, @{thm "Suc_plus1"}]
   @ @{thms add_ac}
- addsimprocs [cancel_div_mod_proc]
+ addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
  val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits 
      [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, 
       @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]