Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added simproc
authorhaftmann
Thu, 16 Apr 2009 14:02:13 +0200
changeset 30936 d13cecf4ed4c
parent 30935 db5dcc1f276d
child 30937 1fe5a573b552
added simproc
src/HOL/Tools/Qelim/presburger.ML file | annotate | diff | comparison | revisions 
--- 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"}]
isabelle